summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2015-08-26 15:49:23 +0200
committerajreynol <andrew.j.reynolds@gmail.com>2015-08-26 15:49:23 +0200
commit7c3790db478c4f06e65ef0f777317a4c6a803059 (patch)
tree89f95e1e0db42a580980b34f58ee1315b73004db /src/smt
parentd9c22c34d122a34d8a8a914936d9186be9a638fe (diff)
Minor improvements to cbqi, fix bug in solving with vts symbols, round up for integer lower bounds. Add presolve infrastructure to quantifiers engine, modify --cbqi-prereg-inst.
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 8fdec25c2..498b2ee12 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1428,6 +1428,9 @@ void SmtEngine::setDefaults() {
if( !options::macrosQuant.wasSetByUser()) {
options::macrosQuant.set( false );
}
+ if( !options::cbqiPreRegInst.wasSetByUser()) {
+ options::cbqiPreRegInst.set( true );
+ }
}
//cbqi options
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback