diff options
Diffstat (limited to 'test/regress/regress0/arith/mult.02.smt2')
-rw-r--r-- | test/regress/regress0/arith/mult.02.smt2 | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/test/regress/regress0/arith/mult.02.smt2 b/test/regress/regress0/arith/mult.02.smt2 deleted file mode 100644 index 57167fc76..000000000 --- a/test/regress/regress0/arith/mult.02.smt2 +++ /dev/null @@ -1,13 +0,0 @@ -; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. -; EXPECT: The fact in question: (>= (* (- 1.0) (* n n)) (- 1.0)) -; EXPECT: ") -; EXIT: 1 -(set-logic QF_LRA) -(set-info :status unknown) -(declare-fun n () Real) - -; This example is test that LRA rejects multiplication terms - -(assert (= (* n n) 1)) - -(check-sat) |