* Add assertion in TheoryModel code to ensure we don't get inconsistent

  substitutions for solved variables.  Related to bug 418 (and might
  resolve it).

* Respect phase-locking in Minisat (one phase-saving site was unguarded).

(this commit was certified error- and warning-free by the test-and-commit script.)

2 files changed, 30 insertions, 4 deletions

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 82d602017..f218332ac 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -260,6 +260,19 @@ Node TheoryModel::getNewDomainValue( TypeNode tn ){
 void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){
   if( !d_substitutions.hasSubstitution( x ) ){
     d_substitutions.addSubstitution( x, t, invalidateCache );
+  } else {
+#ifdef CVC4_ASSERTIONS
+    Node oldX = d_substitutions.getSubstitution(x);
+    // check that either the old substitution is the same, or it now maps to the new substitution
+    if(oldX != t && d_substitutions.apply(oldX) != d_substitutions.apply(t)) {
+      stringstream ss;
+      ss << "Two incompatible substitutions added to TheoryModel:\n"
+         << "the term:    " << x << "\n"
+         << "old mapping: " << d_substitutions.apply(oldX) << "\n"
+         << "new mapping: " << d_substitutions.apply(t);
+      InternalError(ss.str());
+    }
+#endif /* CVC4_ASSERTIONS */
   }
 }
 
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index cf751b69e..5cb8c5e2f 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -108,14 +108,27 @@ public:
   /**
    * Adds a substitution from x to t.
    */
-  void addSubstitution(TNode x, TNode t,
-                       bool invalidateCache = true);
+  void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
 
   /**
    * Returns true iff x is in the substitution map
    */
-  bool hasSubstitution(TNode x)
-    { return d_substitutions.find(x) != d_substitutions.end(); }
+  bool hasSubstitution(TNode x) const {
+    return d_substitutions.find(x) != d_substitutions.end();
+  }
+
+  /**
+   * Returns the substitution mapping that was given for x via
+   * addSubstitution().  Note that the returned value might itself
+   * be in the map; for the actual substitution that would be
+   * performed for x, use .apply(x).  This getSubstitution() function
+   * is mainly intended for constructing assertions about what has
+   * already been put in the map.
+   */
+  TNode getSubstitution(TNode x) const {
+    AssertArgument(hasSubstitution(x), x, "element not in this substitution map");
+    return (*d_substitutions.find(x)).second;
+  }
 
   /**
    * Apply the substitutions to the node.