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 | |
| 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')
| -rw-r--r-- | test/regress/regress0/arith/Makefile.am | 4 | ||||
| -rw-r--r-- | test/regress/regress0/arith/div.09.smt2 | 5 | ||||
| -rw-r--r-- | test/regress/regress0/arith/mult.02.smt2 | 4 |
3 files changed, 9 insertions, 4 deletions
diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index 40f04b239..6c5eded7c 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -35,7 +35,6 @@ TESTS = \ div.06.smt2 \ div.07.smt2 \ div.08.smt2 \ - div.09.smt2 \ mult.01.smt2 \ mult.02.smt2 \ bug443.delta01.smt \ @@ -52,7 +51,8 @@ EXTRA_DIST = $(TESTS) \ miplib-pp08a-3000.smt \ miplib-pp08a-3000.smt2 \ miplib-opt1217--27.smt.expect \ - miplib-pp08a-3000.smt.expect + miplib-pp08a-3000.smt.expect \ + div.09.smt2 #if CVC4_BUILD_PROFILE_COMPETITION #else 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) diff --git a/test/regress/regress0/arith/mult.02.smt2 b/test/regress/regress0/arith/mult.02.smt2 index d690e38e8..54b876d38 100644 --- a/test/regress/regress0/arith/mult.02.smt2 +++ b/test/regress/regress0/arith/mult.02.smt2 @@ -1,4 +1,6 @@ -; EXPECT: (error "Non-linear term was asserted to arithmetic in a linear logic.") +; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. +; EXPECT: The fact in question: (>= (* (- 1) (* n n)) (- 1)) +; EXPECT: ") ; EXIT: 1 (set-logic QF_LRA) (set-info :status unknown) |