mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 05:13:39 +00:00
Code Activity

promote assertion to verify so it triggers in release mode, triggers for bench15

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-01-24 20:15:40 -08:00
parent a2ff185187
commit cf1ce4cea2
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/polysat/op_constraint.cpp
View file

@ -660,7 +660,10 @@ namespace polysat {
pdd prod = p() * r(); pdd prod = p() * r();
rational prodv = (pv * rv).val(); rational prodv = (pv * rv).val();
if (prodv != rational::power_of_two(parity_pv))
verbose_stream() << prodv << " " << rational::power_of_two(parity_pv) << " " << parity_pv << " " << pv << " " << rv << "\n";
SASSERT(prodv != rational::power_of_two(parity_pv)); // Why did it evaluate to false in this case? SASSERT(prodv != rational::power_of_two(parity_pv)); // Why did it evaluate to false in this case?
VERIFY(prodv != rational::power_of_two(parity_pv)); // Why did it evaluate to false in this case?
unsigned lower = 0, upper = m.power_of_2(); unsigned lower = 0, upper = m.power_of_2();
// binary search for the parity (otw. we would have justifications like "parity_at_most(k) && parity_at_least(k)" for at most "k" widths // binary search for the parity (otw. we would have justifications like "parity_at_most(k) && parity_at_least(k)" for at most "k" widths
while (lower + 1 < upper) { while (lower + 1 < upper) {