diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-27 12:26:14 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-08-27 12:26:14 -0500 |
| commit | 11110b87cb70d9c4a6dc486319adbb7dfa59fedb (patch) | |
| tree | 7ce951d48330be5d48deaa280388731d40ef2517 /test | |
| parent | c6aa453fe1c34481f83ca96f5feb8b1a7ad6c734 (diff) | |
Make division chainable in the smt2 parser (#2367)
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
| -rw-r--r-- | test/regress/regress0/arith/div-chainable.smt2 | 12 |
2 files changed, 13 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index f707da219..17a302192 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -15,6 +15,7 @@ REG0_TESTS = \ regress0/arith/div.04.smt2 \ regress0/arith/div.05.smt2 \ regress0/arith/div.07.smt2 \ + regress0/arith/div-chainable.smt2 \ regress0/arith/fuzz_3-eq.smt \ regress0/arith/integers/arith-int-042.cvc \ regress0/arith/integers/arith-int-042.min.cvc \ diff --git a/test/regress/regress0/arith/div-chainable.smt2 b/test/regress/regress0/arith/div-chainable.smt2 new file mode 100644 index 000000000..9ddc80e98 --- /dev/null +++ b/test/regress/regress0/arith/div-chainable.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --rewrite-divk +; EXPECT: sat +(set-logic QF_LIA) +(set-info :status sat) + +(declare-fun x () Int) + +(assert (= (div 4 2 1) 2)) + +(assert (= (div x 2 1) 2)) + +(check-sat) |