diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-02 16:54:10 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-02 16:54:10 +0200 |
| commit | 69769dae4886621f82c2905b82db727bf2e8cf3f (patch) | |
| tree | fde0dfe43acb6fc7f0f07251de91db6ed8c2a148 /src/smt/smt_engine.cpp | |
| parent | d475d255f3c61380524517cd9b97725dcb0c9c22 (diff) | |
On-demand upper bound lemmas for deltas in quantified LRA (for casc). Force no macros-quant in incremental. Update casc TFN script.
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6fdfadbd3..54c97750a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3272,7 +3272,7 @@ void SmtEnginePrivate::processAssertions() { } } dumpAssertions("post-skolem-quant", d_assertions); - if( options::macrosQuant() ){ + if( options::macrosQuant() && !options::incrementalSolving() ){ //quantifiers macro expansion bool success; do{ |