diff options
Diffstat (limited to 'test/regress/regress0/bug519.smt2')
-rw-r--r-- | test/regress/regress0/bug519.smt2 | 76 |
1 files changed, 76 insertions, 0 deletions
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) |