Skip to content

[LRA] Update dom for integers obtained from `select` operations

Hichem R. A. requested to merge hra/int_upd_dom_select into master

I first tried replacing Expr.Base with _ to update the domain for all integers, but it lead to the test slow_convergence_BinaryMultiplication_loop_invariant_inv2_ok_deductible_preserved.psmt2 taking ~ twice as many steps to be solved so I choose to just add select for now

Merge request reports

Loading