diff options
Diffstat (limited to 'test/regress/regress1/push-pop/arith_lra_01.smt2')
| -rw-r--r-- | test/regress/regress1/push-pop/arith_lra_01.smt2 | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/test/regress/regress1/push-pop/arith_lra_01.smt2 b/test/regress/regress1/push-pop/arith_lra_01.smt2 index 4216f429a..79c95b4ab 100644 --- a/test/regress/regress1/push-pop/arith_lra_01.smt2 +++ b/test/regress/regress1/push-pop/arith_lra_01.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental +; COMMAND-LINE: --incremental --no-proof ; EXPECT: sat ; EXPECT: sat ; EXPECT: sat @@ -102,4 +102,3 @@ (assert (or (not (> (+ (* (- 26) x1 ) (* 26 x0 ) ) 48)) (>= (+ (* 35 x3 ) (* (- 43) x2 ) (* 29 x0 ) (* (- 31) x2 ) (* (- 20) x2 ) (* 22 x1 ) ) 49) (>= (+ (* (- 31) x2 ) (* (- 2) x1 ) (* (- 45) x2 ) (* 25 x2 ) (* 29 x4 ) (* (- 23) x1 ) (* (- 1) x0 ) (* 18 x1 ) (* 0 x2 ) (* (- 43) x2 ) (* 24 x2 ) ) (- 23)) )) (assert (or (<= (+ (* 5 x0 ) (* (- 8) x0 ) (* 18 x4 ) (* (- 12) x3 ) (* (- 18) x3 ) (* (- 48) x3 ) (* (- 34) x1 ) (* (- 2) x1 ) (* (- 50) x3 ) (* (- 45) x3 ) ) (- 48)) (>= (+ (* 41 x0 ) (* 25 x2 ) (* (- 17) x2 ) (* (- 6) x0 ) (* (- 48) x3 ) (* (- 36) x3 ) (* 31 x0 ) (* (- 7) x3 ) ) 15) )) (check-sat) - |