From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 26 Jun 2018 22:11:31 +0000 (-0500)
Subject:  Disable uf symmetry breaker in incremental mode (#2091)
X-Git-Tag: cvc5-1.0.0~4944
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b03cb5dc423e83307479e3a513ad6d4abc98d3e9;p=cvc5.git

 Disable uf symmetry breaker in incremental mode (#2091)
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1b5e88536..5652eeaa6 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1657,12 +1657,13 @@ void SmtEngine::setDefaults() {
     }
   }
 
-  // by default, symmetry breaker is on only for QF_UF
+  // by default, symmetry breaker is on only for non-incremental QF_UF
   if(! options::ufSymmetryBreaker.wasSetByUser()) {
-    bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified()
-                 && !options::proof() && !options::unsatCores();
-    Trace("smt") << "setting uf symmetry breaker to " << qf_uf << endl;
-    options::ufSymmetryBreaker.set(qf_uf);
+    bool qf_uf_noinc = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified()
+                       && !options::incrementalSolving() && !options::proof()
+                       && !options::unsatCores();
+    Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc << endl;
+    options::ufSymmetryBreaker.set(qf_uf_noinc);
   }
 
   // If in arrays, set the UF handler to arrays