From cbcc5124a8f0f17acd981a80c182616cd0a778ff Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 1 Jun 2015 22:44:40 +0200
Subject: When proof enabled, disable uf sym break. Add regression.

---
 src/smt/smt_engine.cpp | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

(limited to 'src/smt')

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 11a412c75..9fe3a115d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -700,9 +700,9 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_modelGlobalCommands(),
   d_modelCommands(NULL),
   d_dumpCommands(),
-#ifdef CVC4_PROOF  
+#ifdef CVC4_PROOF
   d_defineCommands(),
-#endif  
+#endif
   d_logic(),
   d_originalOptions(em->getOptions()),
   d_pendingPops(0),
@@ -1083,7 +1083,7 @@ void SmtEngine::setDefaults() {
 
   // by default, symmetry breaker is on only for QF_UF
   if(! options::ufSymmetryBreaker.wasSetByUser()) {
-    bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified();
+    bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified() && !options::proof();
     Trace("smt") << "setting uf symmetry breaker to " << qf_uf << endl;
     options::ufSymmetryBreaker.set(qf_uf);
   }
@@ -1168,8 +1168,8 @@ void SmtEngine::setDefaults() {
   if(! options::repeatSimp.wasSetByUser()) {
     bool repeatSimp = !d_logic.isQuantified() &&
                       (d_logic.isTheoryEnabled(THEORY_ARRAY) &&
-		       d_logic.isTheoryEnabled(THEORY_UF) &&
-		       d_logic.isTheoryEnabled(THEORY_BV)) &&
+                      d_logic.isTheoryEnabled(THEORY_UF) &&
+                      d_logic.isTheoryEnabled(THEORY_BV)) &&
                       !options::unsatCores();
     Trace("smt") << "setting repeat simplification to " << repeatSimp << endl;
     options::repeatSimp.set(repeatSimp);
@@ -1713,7 +1713,7 @@ void SmtEngine::defineFunction(Expr func,
       d_defineCommands.push_back(c.clone());
     });
 
-  
+
   // Substitute out any abstract values in formula
   Expr form = d_private->substituteAbstractValues(Node::fromExpr(formula)).toExpr();
 
@@ -3087,7 +3087,7 @@ void SmtEnginePrivate::processAssertions() {
   Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl;
 
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
-  
+
   if (d_assertions.size() == 0) {
     // nothing to do
     return;
@@ -3385,7 +3385,7 @@ void SmtEnginePrivate::processAssertions() {
           d_iteSkolemMap.erase(toErase.back());
           toErase.pop_back();
         }
-	d_assertions[d_realAssertionsEnd - 1] = Rewriter::rewrite(Node(builder));
+        d_assertions[d_realAssertionsEnd - 1] = Rewriter::rewrite(Node(builder));
       }
       // For some reason this is needed for some benchmarks, such as
       // http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
@@ -3497,7 +3497,7 @@ void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput)
     }
     // rewrite rules are by default in the unsat core because
     // they need to be applied until saturation
-    if(options::unsatCores() && 
+    if(options::unsatCores() &&
        n.getKind() == kind::REWRITE_RULE ){
       ProofManager::currentPM()->addUnsatCore(n.toExpr());
     }
@@ -4030,8 +4030,8 @@ void SmtEngine::checkUnsatCore() {
   for (; itg != d_defineCommands.end();  ++itg) {
     (*itg)->invoke(&coreChecker);
   }
-	);
-  
+  );
+
   Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core.size() << ")" << endl;
   for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
     Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i << endl;
-- 
cgit v1.2.3