projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b721666) | patch
Fix issues with bv2nat (#2219)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 1 Aug 2018 17:22:09 +0000 (12:22 -0500)
committerAndres Noetzli <andres.noetzli@gmail.com>
Wed, 1 Aug 2018 17:22:09 +0000 (10:22 -0700)
commit0aa6e039827750757941751e0829575a55601ace
tree25e21dfd16e232e07615791935bfc6c32fc5bcabtree
parentb721666fd7a2dafaaeb112059c2588c99e8020eccommit | diff
Fix issues with bv2nat (#2219)

This includes:
- A missing case in the smt2 printer,
- A bug in an inference of int2bv applied to bv2nat where the types are different.
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/theory/bv/theory_bv.cpp diff | blob | history
src/theory/bv/theory_bv.h diff | blob | history
test/regress/Makefile.tests diff | blob | history
test/regress/regress1/bv/bv2nat-types.smt2 [new file with mode: 0644] blob