From 69769dae4886621f82c2905b82db727bf2e8cf3f Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 2 Jul 2015 16:54:10 +0200
Subject: On-demand upper bound lemmas for deltas in quantified LRA (for casc).
 Force no macros-quant in incremental. Update casc TFN script.

---
 src/smt/smt_engine.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/smt/smt_engine.cpp')

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{
-- 
cgit v1.2.3