diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-24 19:35:58 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-24 20:07:39 -0400 |
| commit | 0a3422299da7e882bae22c5fa3e5ec3c80b42046 (patch) | |
| tree | d00f31a33f03f11608ee046b851f4c63e194fe87 /test/regress/regress0/arith/div.09.smt2 | |
| parent | 30d21b25af6ee619e5f53d1ca8821b710fad4cb7 (diff) | |
Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk allows linearization of div,mod,/ by a constant.
Diffstat (limited to 'test/regress/regress0/arith/div.09.smt2')
| -rw-r--r-- | test/regress/regress0/arith/div.09.smt2 | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/test/regress/regress0/arith/div.09.smt2 b/test/regress/regress0/arith/div.09.smt2 index 2f1bca63a..9bcb93476 100644 --- a/test/regress/regress0/arith/div.09.smt2 +++ b/test/regress/regress0/arith/div.09.smt2 @@ -1,4 +1,7 @@ -; EXPECT: (error "Non-linear term was asserted to arithmetic in a linear logic.") +; EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (/ n n) +; EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +; EXPECT: The fact in question: (>= (+ (* (- 1) (/ n n)) termITE_132) 0) +; EXPECT: ") ; EXIT: 1 (set-logic QF_LRA) (set-info :status unknown) |