projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: dc38452) | patch
Adding tests for get-value output for arithmetic.
authorTim King <tim.king@imag.fr>
Mon, 19 Jan 2015 17:57:29 +0000 (18:57 +0100)
committerTim King <tim.king@imag.fr>
Mon, 19 Jan 2015 18:05:04 +0000 (19:05 +0100)
commit66daf10d1bf4cb2f1846f599fe11e27312ac2069
tree575c7abb8c2db919fbd437d11dfe48f82d2c363btree
parentdc38452fb64b58c96c73b8bcab7d89fc86b0ecddcommit | diff
Adding tests for get-value output for arithmetic.

Fixing bug where (- 1).0 was printed by get-value. Thanks to Christoph Sticksel for the bug report.
src/printer/smt2/smt2_printer.cpp diff | blob | history
test/regress/regress0/Makefile.am diff | blob | history
test/regress/regress0/get-value-ints.smt2 [new file with mode: 0644] blob
test/regress/regress0/get-value-reals-ints.smt2 [new file with mode: 0644] blob
test/regress/regress0/get-value-reals.smt2 [new file with mode: 0644] blob