Fix for bug 519; don't involve ITESimplifier in model generation.

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 08be411718b4f88ee88203ab57c27760c690c4bb..b10c85cfe82d292807bdcdb778f97cdc67fdd2e5 100644 (file)
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -102,9 +102,6 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
     if(n.getKind() == kind::LAMBDA) {
       NodeManager* nm = NodeManager::currentNM();
       Node body = getModelValue(n[1], true);
-      // This is a bit ugly, but cache inside simplifier can change, so can't be const
-      // The ite simplifier is needed to get rid of artifacts created by Boolean terms
-      body = const_cast<ITESimplifier*>(&d_iteSimp)->simpITE(body);
       body = Rewriter::rewrite(body);
       return nm->mkNode(kind::LAMBDA, n[0], body);
     }

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index f1d69010f3aff143770852960748759f6b9d65fd..e380f2fc203a9fbaf6ab37184912428ee69eecba 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -153,7 +153,8 @@ BUG_TESTS = \
        bug497.cvc \
        bug507.smt2 \
        bug512.smt2 \
-       bug512.minimized.smt2
+       bug512.minimized.smt2 \
+       bug519.smt2
 
 TESTS =        $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 

diff --git a/test/regress/regress0/bug519.smt2 b/test/regress/regress0/bug519.smt2
new file mode 100644 (file)
index 0000000..b3a2950
--- /dev/null
+++ b/test/regress/regress0/bug519.smt2
@@ -0,0 +1,76 @@
+; COMMAND-LINE: -mi
+; EXPECT: unknown
+; EXPECT: unsat
+; EXIT: 20
+
+(set-logic ALL_SUPPORTED)
+
+; must make parts 1 through 6 with different deadlines
+
+; part 1 must be available for part 2
+; parts 3 and 4 must be available for part 5
+; all parts must be available for part 6
+
+; start/complete is the timestep when a part is started/finished
+(declare-fun start (Int) Int)
+(declare-fun complete (Int) Int)
+
+(define-fun before ((i Int) (j Int)) Bool (< (complete i) (start j)))
+
+(assert (before 1 2))
+(assert (before 3 5))
+(assert (before 4 5))
+(assert (before 1 6))
+(assert (before 2 6))
+(assert (before 3 6))
+(assert (before 4 6))
+(assert (before 5 6))
+
+; part 1 takes 2 units of time
+; part 2 takes 3
+; part 3 takes 3
+; part 4 takes 1
+; part 5 takes 2
+; part 6 takes 1
+
+(define-fun requires ((i Int) (j Int)) Bool (= (complete i) (+ (start i) j)))
+
+(assert (requires 1 2))
+(assert (requires 2 3))
+(assert (requires 3 3))
+(assert (requires 4 1))
+(assert (requires 5 2))
+(assert (requires 6 1))
+
+(assert (>= (start 1) 0))
+(assert (>= (start 2) 0))
+(assert (>= (start 3) 0))
+(assert (>= (start 4) 0))
+(assert (>= (start 5) 0))
+(assert (>= (start 6) 0))
+
+(define-fun cost () Int (complete 6))
+
+(define-fun parallel ((t Int)) Int
+            (+ (ite (<= (start 1) t (complete 1)) 1 0)
+               (ite (<= (start 2) t (complete 2)) 1 0)
+               (ite (<= (start 3) t (complete 3)) 1 0)
+               (ite (<= (start 4) t (complete 4)) 1 0)
+               (ite (<= (start 5) t (complete 5)) 1 0)
+               (ite (<= (start 6) t (complete 6)) 1 0)))
+
+(declare-fun cost2 () Int)
+(assert (= cost2 cost))
+
+(declare-fun max-parallel () Int)
+(assert (forall ((t Int)) (=> (<= 0 t cost2) (>= max-parallel (parallel t)))))
+
+(check-sat)
+;(get-model)
+;(get-value (cost2))
+;(get-value ((parallel 1)))
+;(get-value ((=> (<= 0 1 cost2) (>= max-parallel (parallel 1)))))
+
+(assert (< cost 8))
+
+(check-sat)