projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 66836c5)
Fix unsupported option in regress1. (#4874)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 12 Aug 2020 06:41:45 +0000 (01:41 -0500)
committerGitHub <noreply@github.com>
Wed, 12 Aug 2020 06:41:45 +0000 (23:41 -0700)
Fixes regress1.

test/regress/regress1/quantifiers/issue4021-ind-opts.smt2 patch | blob | history

diff --git a/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2 b/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2
index c9d4eb0340d5882f54dd599907e624e138621a44..03bbd9469554eef3145e6d8424c5989f173dc533 100644 (file)
--- a/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2
+++ b/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2
@@ -2,7 +2,6 @@
 (set-option :ag-miniscope-quant true)
 (set-option :conjecture-gen true)
 (set-option :int-wf-ind true)
-(set-option :quant-model-ee true)
 (set-option :sygus-inference true)
 (set-option :uf-ho true)
 (set-info :status unsat)