projects
/
cvc5.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
| inline |
side by side
Fix unsupported option in regress1. (#4874)
[cvc5.git]
/
test
/
regress
/
regress1
/
quantifiers
/
issue4021-ind-opts.smt2
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)