From 22c270963b48dae4e306972026c8accf7c9a6765 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 11 Oct 2012 21:17:12 +0000
Subject: [PATCH] Fix bug 421, again, and add a second, independent test case
 for the same with --check-models (which caused the same bug, for a different
 reason, due to some unintended interaction between the checkModel() function
 and the UserContext, which rolled back the Model object.  (Groan...)

(this commit was certified error- and warning-free by the test-and-commit script.)
---
 src/smt/smt_engine.cpp             | 28 +++++++++++++++++++---------
 test/regress/regress0/Makefile.am  |  3 ++-
 test/regress/regress0/bug421b.smt2 | 15 +++++++++++++++
 3 files changed, 36 insertions(+), 10 deletions(-)
 create mode 100644 test/regress/regress0/bug421b.smt2

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 84f8c4f95..fa619c653 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -390,7 +390,21 @@ public:
     throw(TypeCheckingException);
 
   /**
-   * pre-skolemize quantifiers
+   * Simplify node "in" by expanding definitions and applying any
+   * substitutions learned from preprocessing.
+   */
+  Node simplify(TNode in) {
+    // Substitute out any abstract values in ex.
+    // Expand definitions.
+    hash_map<Node, Node, NodeHashFunction> cache;
+    Node n = expandDefinitions(in, cache).toExpr();
+    // Make sure we've done all preprocessing, etc.
+    Assert(d_assertionsToCheck.size() == 0 && d_assertionsToPreprocess.size() == 0);
+    return applySubstitutions(n).toExpr();
+  }
+
+  /**
+   * Pre-skolemize quantifiers.
    */
   Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector<Node>& fvs);
 
@@ -2094,18 +2108,14 @@ Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException) {
     Dump("benchmark") << SimplifyCommand(ex);
   }
 
-  // Substitute out any abstract values in ex.
   Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
   if( options::typeChecking() ) {
     e.getType(true);// ensure expr is type-checked at this point
   }
-  // Expand definitions.
-  hash_map<Node, Node, NodeHashFunction> cache;
-  e = d_private->expandDefinitions(Node::fromExpr(e), cache).toExpr();
-  // Make sure we've done simple preprocessing, unit detection, etc.
-  Trace("smt") << "SmtEngine::check(): processing assertions" << endl;
+
+  // Make sure all preprocessing is done
   d_private->processAssertions();
-  return d_private->applySubstitutions(e).toExpr();
+  return d_private->simplify(Node::fromExpr(e)).toExpr();
 }
 
 Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException) {
@@ -2424,7 +2434,7 @@ void SmtEngine::checkModel(bool hardFailure) {
     Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << endl;
 
     // Simplify the result.
-    n = Node::fromExpr(simplify(n.toExpr()));
+    n = d_private->simplify(n);
     Notice() << "SmtEngine::checkModel(): -- simplifies to  " << n << endl;
 
     TheoryId thy = Theory::theoryOf(n);
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index de1c8eca5..4a4f02d91 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -132,7 +132,8 @@ BUG_TESTS = \
 	bug382.smt2 \
 	bug383.smt2 \
 	bug398.smt2 \
-	bug421.smt2
+	bug421.smt2 \
+	bug421b.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/bug421b.smt2 b/test/regress/regress0/bug421b.smt2
new file mode 100644
index 000000000..a47efb6fb
--- /dev/null
+++ b/test/regress/regress0/bug421b.smt2
@@ -0,0 +1,15 @@
+; same as bug421.smt2 but adds --check-models on command line:
+; this actually caused the same bug for a different reason, so
+; we check them both independently in regressions
+;
+; COMMAND-LINE: --incremental --abstract-values --check-models
+; EXPECT: sat
+; EXPECT: ((a @1) (b @2))
+; EXIT: 10
+(set-logic QF_AUFLIA)
+(set-option :produce-models true)
+(declare-fun a () (Array Int Int))
+(declare-fun b () (Array Int Int))
+(assert (not (= a b)))
+(check-sat)
+(get-value (a b))
-- 
2.30.2