From 804c83d332c9e8c909e7009e93eeefd5200e8b39 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 9 Jul 2013 21:22:53 -0400
Subject: [PATCH] Fix for bug 519; don't involve ITESimplifier in model
 generation.

---
 src/theory/model.cpp              |  3 --
 test/regress/regress0/Makefile.am |  3 +-
 test/regress/regress0/bug519.smt2 | 76 +++++++++++++++++++++++++++++++
 3 files changed, 78 insertions(+), 4 deletions(-)
 create mode 100644 test/regress/regress0/bug519.smt2

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 08be41171..b10c85cfe 100644
--- 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 f1d69010f..e380f2fc2 100644
--- 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
index 000000000..b3a2950a6
--- /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)
-- 
2.30.2