projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 85a3056) | patch
bv2int: support models in tests (#5068)
authoryoni206 <yoni206@users.noreply.github.com>
Wed, 16 Sep 2020 04:31:10 +0000 (21:31 -0700)
committerGitHub <noreply@github.com>
Wed, 16 Sep 2020 04:31:10 +0000 (23:31 -0500)
commite61c6ecf2e8c569d9f1b5f27ec1309371cc45cff
tree339ec96158b78b7e998a6c4edd16a4127a7fe8aatree
parent85a3056bed70e226d9e17a1f5785d957628f9e26commit | diff
bv2int: support models in tests (#5068)

Previous changes in this preprocessing pass have already enabled model generation when using it.
However, the satisfiable tests still had --no-check-models.

The changes in this PR:

All --no-check-models from current tests for the preprocessing pass are removed.
Refactoring of the relevant part of the code.
Solves CVC4/cvc4-projects#128.

Remark: disabling white-spaces when reviewing this PR is recommended.
17 files changed:
src/preprocessing/passes/bv_to_int.cpp diff | blob | history
src/preprocessing/passes/bv_to_int.h diff | blob | history
test/regress/regress0/bv/bv_to_int1.smt2 diff | blob | history
test/regress/regress0/bv/bv_to_int2.smt2 diff | blob | history
test/regress/regress0/bv/bv_to_int_bitwise.smt2 diff | blob | history
test/regress/regress0/bv/bv_to_int_bvmul1.smt2 diff | blob | history
test/regress/regress0/bv/bv_to_int_bvmul2.smt2 diff | blob | history
test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 diff | blob | history
test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 diff | blob | history
test/regress/regress0/bv/bv_to_int_elim_err.smt2 diff | blob | history
test/regress/regress0/bv/bv_to_int_zext.smt2 diff | blob | history
test/regress/regress2/bv_to_int_ashr.smt2 diff | blob | history
test/regress/regress2/bv_to_int_mask_array_1.smt2 diff | blob | history
test/regress/regress2/bv_to_int_mask_array_2.smt2 diff | blob | history
test/regress/regress2/bv_to_int_mask_array_3.smt2 diff | blob | history
test/regress/regress2/bv_to_int_shifts.smt2 diff | blob | history
test/regress/regress3/bv_to_int_and_or.smt2 diff | blob | history