summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2015-05-11 20:06:21 +0200
committerajreynol <andrew.j.reynolds@gmail.com>2015-05-11 20:06:21 +0200
commit54f1d00d5475710ec5a4c3eab82d786ba95dfdde (patch)
tree547bd29a009a3d119a26b2ddcd509a3ef2e5d061 /src/smt
parent870b29b0cce85941ed72d7e0ca75b61b0cfcf711 (diff)
Allow sygus with no syntactic restrictions for LIA. Add regressions.
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/smt_engine.cpp3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b20b84690..bc594a47e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1399,6 +1399,9 @@ void SmtEngine::setDefaults() {
options::ceGuidedInst.set( true );
}
if( options::ceGuidedInst() ){
+ if( !options::cegqiSingleInv.wasSetByUser() ){
+ options::cegqiSingleInv.set( true );
+ }
if( !options::quantConflictFind.wasSetByUser() ){
options::quantConflictFind.set( false );
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback