projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 39e395e) | patch
bv2int: quantifiers support (#5080)
authoryoni206 <yoni206@users.noreply.github.com>
Fri, 18 Sep 2020 17:12:04 +0000 (10:12 -0700)
committerGitHub <noreply@github.com>
Fri, 18 Sep 2020 17:12:04 +0000 (12:12 -0500)
commitf92c4476e335322c1eeaa9e15ff5e1fda06181fe
tree9d5d1bd2fe539314fe5ff030533f7f5b2b517781tree
parent39e395e08646efb2fc0e352bfc110563afbd9043commit | diff
bv2int: quantifiers support (#5080)

This PR adds quantifiers support for bv2int preprocessing pass, and adds regressions that use quantifiers.
src/preprocessing/passes/bv_to_int.cpp diff | blob | history
src/preprocessing/passes/bv_to_int.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2 [new file with mode: 0644] blob
test/regress/regress3/bv_to_int_check_ne_bvlshr0_4bit.smt2.minimized.smt2 [new file with mode: 0644] blob
test/regress/regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2 [new file with mode: 0644] blob