diff options
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) |