mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

Removed wrong assertion

Browse source
This commit is contained in:
Clemens Eisenhofer 2023-01-27 08:32:44 +01:00
parent 88d11c9381
commit e8163b1769
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -662,8 +662,6 @@ namespace polysat {
rational prodv = (pv * rv).val(); rational prodv = (pv * rv).val();
if (prodv != rational::power_of_two(parity_pv)) if (prodv != rational::power_of_two(parity_pv))
verbose_stream() << prodv << " " << rational::power_of_two(parity_pv) << " " << parity_pv << " " << pv << " " << rv << "\n"; 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?
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) {
@ -688,6 +686,7 @@ namespace polysat {
if (rv.val() > max_rv) if (rv.val() > max_rv)
return s.mk_clause(~invc, s.parity_at_least(p(), middle), s.ule(r(), max_rv), false); return s.mk_clause(~invc, s.parity_at_least(p(), middle), s.ule(r(), max_rv), false);
} }
// Why did it evaluate to false in this case?
UNREACHABLE(); UNREACHABLE();
return {}; return {};
} }