projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0403940) | patch
Fix issues with real to int (#3918)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 5 Mar 2020 20:38:16 +0000 (14:38 -0600)
committerGitHub <noreply@github.com>
Thu, 5 Mar 2020 20:38:16 +0000 (14:38 -0600)
commitd26ee67911fedfef966a0e4d64ffda02007d65a0
treed8d5511eeb12ecace73845785546df95e8f67f1ftree
parent04039407e6308070c148de0d5e93640ec1b0a341commit | diff
Fix issues with real to int (#3918)

This fixes a few issues in the real to int preprocessing pass. Previously it was not robust to cases where the input had constraints that were not over the reals.

Fixes #3915 and fixes #3913 and fixes #3916.
src/preprocessing/passes/real_to_int.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/push-pop/issue3915-real-as-int.smt2 [new file with mode: 0644] blob
test/regress/regress1/quantifiers/real-to-int-quant.smt2 [new file with mode: 0644] blob