diff options
Diffstat (limited to 'test/regress/regress0/expect/scrub.02.smt')
| -rw-r--r-- | test/regress/regress0/expect/scrub.02.smt | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/test/regress/regress0/expect/scrub.02.smt b/test/regress/regress0/expect/scrub.02.smt new file mode 100644 index 000000000..f2e6554b7 --- /dev/null +++ b/test/regress/regress0/expect/scrub.02.smt @@ -0,0 +1,13 @@ +% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' +% 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: TERM +% EXPECT: ") +% EXIT: 1 +(benchmark reject_nonlinear +:logic QF_LRA +:extrafuns ((n Real)) +:status unknown +:formula +(= (/ n n) 1) +) |