diff options
| author | Tim King <taking@google.com> | 2017-04-02 19:29:36 -0700 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2017-04-02 19:29:36 -0700 |
| commit | f278f060c177593a1835422e688fe2a022c40e2f (patch) | |
| tree | cc2eaa62bfc4c581643cbd237d93247b8c40134f /test/regress/regress0/arith | |
| parent | e9f3b6a54e4bf35f915c46d822ed9ee051cc7df3 (diff) | |
Adding a model based axiom instantiation scheme for multiplication. Merge commit for nlAlgMaster.
Diffstat (limited to 'test/regress/regress0/arith')
| -rw-r--r-- | test/regress/regress0/arith/bug716.0.smt2 | 3 | ||||
| -rw-r--r-- | test/regress/regress0/arith/div.09.smt2 | 3 |
2 files changed, 2 insertions, 4 deletions
diff --git a/test/regress/regress0/arith/bug716.0.smt2 b/test/regress/regress0/arith/bug716.0.smt2 index 20a5ca3f0..d5df938a7 100644 --- a/test/regress/regress0/arith/bug716.0.smt2 +++ b/test/regress/regress0/arith/bug716.0.smt2 @@ -1,6 +1,5 @@ ; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/' -; EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: TERM -; 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: (error "A non-linear fact was asserted to arithmetic in a linear logic. ; EXPECT: The fact in question: TERM ; EXPECT: ") ; EXIT: 1 diff --git a/test/regress/regress0/arith/div.09.smt2 b/test/regress/regress0/arith/div.09.smt2 index e457734eb..1c4bbde2b 100644 --- a/test/regress/regress0/arith/div.09.smt2 +++ b/test/regress/regress0/arith/div.09.smt2 @@ -1,6 +1,5 @@ ; 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: (error "A non-linear fact was asserted to arithmetic in a linear logic. ; EXPECT: The fact in question: TERM ; EXPECT: ") ; EXIT: 1 |