diff options
Diffstat (limited to 'test/regress/regress1/arith/arith-brab-test.smt2')
| -rw-r--r-- | test/regress/regress1/arith/arith-brab-test.smt2 | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/test/regress/regress1/arith/arith-brab-test.smt2 b/test/regress/regress1/arith/arith-brab-test.smt2 new file mode 100644 index 000000000..7856ae0e6 --- /dev/null +++ b/test/regress/regress1/arith/arith-brab-test.smt2 @@ -0,0 +1,23 @@ +; COMMAND-LINE: --arith-brab +; COMMAND-LINE: --no-arith-brab +; EXPECT: sat +(set-logic ALL) + +(declare-fun x1 () Real) +(declare-fun y1 () Real) +(declare-fun m1 () Real) +(declare-fun b1 () Real) + +(declare-fun x () Int) +(declare-fun y () Int) + +(assert (= y1 (+ b1 (* m1 x1)))) +(assert (= x1 (/ m1 (- y1 b1)))) +(assert (= b1 1.25)) +(assert (= m1 (/ 1 3))) + +(assert (and (> x x1) (> y y1))) + +(check-sat) +(exit) + |