projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 35b0536) | patch
int-to-bv: fail if one of the arguments has type real (#7810)
authoryoni206 <yoni206@users.noreply.github.com>
Thu, 16 Dec 2021 15:52:09 +0000 (17:52 +0200)
committerGitHub <noreply@github.com>
Thu, 16 Dec 2021 15:52:09 +0000 (15:52 +0000)
commit60973169af7ad8653436fc6497e13e25897ed578
treee37f6e311f675adf60c5c6a99fb9c36202df82e1tree
parent35b05367c5caa47f4be367c257b4a9c411ebfd38commit | diff
int-to-bv: fail if one of the arguments has type real (#7810)

This PR generates a failure in int-to-bv in case a real argument is detected as a child of an arithmetic operation.
fixes cvc5/cvc5-projects#348 .

Co-authored-by: Andrew Reynolds andrew.j.reynolds@gmail.com
src/preprocessing/passes/int_to_bv.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/nl/proj-issue-348.smt2 [new file with mode: 0644] blob