1 file changed
+1
-1
lines changed- .github/workflows/pull-request-checks.yaml+6-6
- CHANGELOG+24
- regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c+6-3
- regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c+6-3
- regression/contracts-dfcc/invar_havoc_dynamic_array_const_idx/main.c+1-1
- regression/contracts-dfcc/invar_loop-entry_check/main.c+4-3
- regression/contracts-dfcc/invar_loop-entry_check/test.desc+4-4
- regression/contracts-dfcc/invar_loop-entry_fail/main.c+1-1
- regression/contracts-dfcc/loop_assigns_inference-01/test.desc+5-5
- regression/contracts-dfcc/loop_assigns_inference-03/main.c+1-1
- regression/contracts-dfcc/loop_assigns_inference-04/main.c+22
- regression/contracts-dfcc/loop_assigns_inference-04/test.desc+14
- regression/contracts-dfcc/loop_assigns_inference-05/main.c+17
- regression/contracts-dfcc/loop_assigns_inference-05/test.desc+15
- regression/contracts/loop_assigns_inference-04/main.c+22
- regression/contracts/loop_assigns_inference-04/test.desc+10
- src/config.inc+1-1
- src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp+47-32
- src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h+2
- src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp+284-11
- src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.h+21-6
- src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp+2
- src/goto-instrument/loop_utils.cpp+61-9
- src/libcprover-rust/Cargo.toml+1-1
- src/solvers/flattening/boolbv.cpp+2
- src/solvers/floatbv/float_bv.cpp+5-3
- src/solvers/smt2/smt2_conv.cpp+4
- src/solvers/smt2_incremental/convert_expr_to_smt.cpp+13
- src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp+16-2
- src/util/bitvector_expr.cpp+30-3
- src/util/bitvector_expr.h+44
- src/util/format_expr.cpp+6
- src/util/irep_ids.def+1
- src/util/lower_byte_operators.cpp+10-9
- src/util/simplify_expr.cpp+4
- src/util/simplify_expr_class.h+2
- src/util/simplify_expr_int.cpp+12
- unit/Makefile+1
- unit/solvers/flattening/boolbv_update_bit.cpp+48
0 commit comments