projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e648859) | patch
Int2BV fail on demand (#4079)
authoryoni206 <yoni206@users.noreply.github.com>
Tue, 24 Mar 2020 17:53:18 +0000 (10:53 -0700)
committerGitHub <noreply@github.com>
Tue, 24 Mar 2020 17:53:18 +0000 (12:53 -0500)
commitd19b800ac00feb44bfc6302f02695c8700e15c12
tree4272602a77c69b5ecc4a82c83561b20e02679e76tree
parente648859c74339fb1b5838c6d439e9dfa1f490bcccommit | diff
Int2BV fail on demand (#4079)

This PR delays error on unsupported symbols as much as possible, by only throwing the error when actually constructing the node.
contrib/competitions/smt-comp/run-script-smtcomp-current diff | blob | history
src/preprocessing/passes/int_to_bv.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/bv/bv-abstr-bug2.smt2 diff | blob | history
test/regress/regress0/bv/int_to_bv_err_on_demand_1.smt2 [new file with mode: 0644] blob