Merge branch '1.2.x'

Conflicts:
	library_versions
	src/parser/parser.h

2 files changed, 36 insertions, 24 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ab4b13d4c..ca89ce36d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -823,15 +823,6 @@ void SmtEngine::setLogicInternal() throw() {
 
   d_logic.lock();
 
-  // may need to force uninterpreted functions to be on for non-linear
-  if(((d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()) ||
-      d_logic.isTheoryEnabled(THEORY_BV)) &&
-     !d_logic.isTheoryEnabled(THEORY_UF)){
-    d_logic = d_logic.getUnlockedCopy();
-    d_logic.enableTheory(THEORY_UF);
-    d_logic.lock();
-  }
-
   // Set the options for the theoryOf
   if(!options::theoryOfMode.wasSetByUser()) {
     if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV)) {
@@ -1322,6 +1313,11 @@ Node SmtEnginePrivate::expandBVDivByZero(TNode n) {
   Node divTotalNumDen = nm->mkNode(n.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL :
                                    kind::BITVECTOR_UREM_TOTAL, num, den);
   Node node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
+  if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) {
+    d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+    d_smt.d_logic.enableTheory(THEORY_UF);
+    d_smt.d_logic.lock();
+  }
   return node;
 }
 
@@ -1372,13 +1368,14 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
   }
   case kind::DIVISION: {
     // partial function: division
-    if(d_smt.d_logic.isLinear()) {
-      node = n;
-      break;
-    }
     if(d_divByZero.isNull()) {
       d_divByZero = nm->mkSkolem("divByZero", nm->mkFunctionType(nm->realType(), nm->realType()),
                                  "partial real division", NodeManager::SKOLEM_EXACT_NAME);
+      if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) {
+        d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+        d_smt.d_logic.enableTheory(THEORY_UF);
+        d_smt.d_logic.lock();
+      }
     }
     TNode num = n[0], den = n[1];
     Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
@@ -1390,13 +1387,14 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
 
   case kind::INTS_DIVISION: {
     // partial function: integer div
-    if(d_smt.d_logic.isLinear()) {
-      node = n;
-      break;
-    }
     if(d_intDivByZero.isNull()) {
       d_intDivByZero = nm->mkSkolem("intDivByZero", nm->mkFunctionType(nm->integerType(), nm->integerType()),
                                     "partial integer division", NodeManager::SKOLEM_EXACT_NAME);
+      if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) {
+        d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+        d_smt.d_logic.enableTheory(THEORY_UF);
+        d_smt.d_logic.lock();
+      }
     }
     TNode num = n[0], den = n[1];
     Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
@@ -1408,13 +1406,14 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
 
   case kind::INTS_MODULUS: {
     // partial function: mod
-    if(d_smt.d_logic.isLinear()) {
-      node = n;
-      break;
-    }
     if(d_modZero.isNull()) {
       d_modZero = nm->mkSkolem("modZero", nm->mkFunctionType(nm->integerType(), nm->integerType()),
                                "partial modulus", NodeManager::SKOLEM_EXACT_NAME);
+      if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) {
+        d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+        d_smt.d_logic.enableTheory(THEORY_UF);
+        d_smt.d_logic.lock();
+      }
     }
     TNode num = n[0], den = n[1];
     Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
@@ -3639,6 +3638,11 @@ void SmtEngine::push() throw(ModalException, LogicException) {
     d_needPostsolve = false;
   }
 
+  // The problem isn't really "extended" yet, but this disallows
+  // get-model after a push, simplifying our lives somewhat and
+  // staying symmtric with pop.
+  d_problemExtended = true;
+
   d_userLevels.push_back(d_userContext->getLevel());
   internalPush();
   Trace("userpushpop") << "SmtEngine: pushed to level "
@@ -3665,6 +3669,14 @@ void SmtEngine::pop() throw(ModalException) {
     d_needPostsolve = false;
   }
 
+  // The problem isn't really "extended" yet, but this disallows
+  // get-model after a pop, simplifying our lives somewhat.  It might
+  // not be strictly necessary to do so, since the pops occur lazily,
+  // but also it would be weird to have a legally-executed (get-model)
+  // that only returns a subset of the assignment (because the rest
+  // is no longer in scope!).
+  d_problemExtended = true;
+
   AlwaysAssert(d_userContext->getLevel() > 0);
   AlwaysAssert(d_userLevels.back() < d_userContext->getLevel());
   while (d_userLevels.back() < d_userContext->getLevel()) {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 8266bb1ed..1b5af415f 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -189,9 +189,9 @@ class CVC4_PUBLIC SmtEngine {
   bool d_fullyInited;
 
   /**
-   * Whether or not we have added any assertions/declarations/definitions
-   * since the last checkSat/query (and therefore we're not responsible
-   * for an assignment).
+   * Whether or not we have added any assertions/declarations/definitions,
+   * or done push/pop, since the last checkSat/query, and therefore we're
+   * not responsible for models or proofs.
    */
   bool d_problemExtended;