Resolve "provide axioms for sdiv and smod in theory bitvector theory"
commit6ce01d8b7e58fa6f13fa267677bc297feb1fec78
authorMARCHE Claude <claude.marche@inria.fr>
Sat, 2 Nov 2024 07:36:31 +0000 (2 08:36 +0100)
committerMARCHE Claude <claude.marche@inria.fr>
Sat, 2 Nov 2024 07:36:31 +0000 (2 08:36 +0100)
tree0694d77aeaa0236a502c9db85db242d596c5340e
parentda82f89b3feec6a479afe66fbb68b32aaafdf58e
Resolve "provide axioms for sdiv and smod in theory bitvector theory"
33 files changed:
bench/check-ce-bench
bench/check-ce/oracles/640_no_loc_failure_Alt-Ergo,2.5.4_SP.oracle
bench/check-ce/oracles/640_no_loc_failure_Alt-Ergo,2.5.4_WP.oracle
bench/check-ce/oracles/657_Alt-Ergo,2.5.4_SP.oracle
bench/check-ce/oracles/657_Alt-Ergo,2.5.4_WP.oracle
bench/check-ce/oracles/668_projection_Alt-Ergo,2.5.4_SP.oracle
bench/check-ce/oracles/668_projection_Alt-Ergo,2.5.4_WP.oracle
bench/check-ce/oracles/703_reduce_term_Alt-Ergo,2.5.4_SP.oracle
bench/check-ce/oracles/703_reduce_term_Alt-Ergo,2.5.4_WP.oracle
bench/check-ce/oracles/bv32_Alt-Ergo,2.5.4_SP.oracle
bench/check-ce/oracles/bv32_Alt-Ergo,2.5.4_WP.oracle
bench/check-ce/oracles/bv32_CVC4,1.8_SP.oracle
bench/check-ce/oracles/bv32_CVC4,1.8_WP.oracle
bench/check-ce/oracles/bv32_mono_Alt-Ergo,2.5.4_SP.oracle
bench/check-ce/oracles/bv32_mono_Alt-Ergo,2.5.4_WP.oracle
bench/check-ce/oracles/bv32_mono_CVC4,1.8_SP.oracle
bench/check-ce/oracles/bv32_mono_CVC4,1.8_WP.oracle
bench/check-ce/oracles/bv32_toBig_Alt-Ergo,2.5.4_SP.oracle
bench/check-ce/oracles/bv32_toBig_Alt-Ergo,2.5.4_WP.oracle
bench/check-ce/oracles/map_of_algebraic_Alt-Ergo,2.5.4_SP.oracle
bench/check-ce/oracles/map_of_algebraic_Alt-Ergo,2.5.4_WP.oracle
bench/check-ce/oracles/threshold_Alt-Ergo,2.5.4_SP.oracle
bench/check-ce/oracles/threshold_Alt-Ergo,2.5.4_WP.oracle
bench/check-ce/oracles/threshold_CVC4,1.8_SP.oracle
bench/check-ce/oracles/threshold_CVC4,1.8_WP.oracle
bench/check-ce/oracles/threshold_CVC5,1.0.5_SP.oracle
bench/check-ce/oracles/threshold_CVC5,1.0.5_WP.oracle
drivers/smt-libv2-bv-realization.gen
drivers/smt-libv2-bv.gen
lib/coq/bv/BV_Gen.v
src/driver/call_provers.ml
stdlib/bv.mlw
stdlib/mach/bv.mlw