diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-03-04 10:39:27 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-03-04 10:39:38 +0100 |
| commit | 74f1358ca108f3ae4bc8b2d01a2c14e0c20bcc9b (patch) | |
| tree | ffcd22bc1205e4619e05af2eac79918287af2374 /src/smt | |
| parent | f6833bca76627f970d3c61ee163a32869ffa1b10 (diff) | |
More work on arithmetic single invocation synthesis conjectures.
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3aec77a45..8ad321602 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1353,6 +1353,9 @@ void SmtEngine::setDefaults() { if( !options::quantConflictFind.wasSetByUser() ){ options::quantConflictFind.set( false ); } + if( !options::instNoEntail.wasSetByUser() ){ + options::instNoEntail.set( false ); + } //do not allow partial functions if( !options::bitvectorDivByZeroConst.wasSetByUser() ){ options::bitvectorDivByZeroConst.set( true ); |