* 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.)

1 files changed, 17 insertions, 4 deletions

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.