mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 06:43:40 +00:00
Code Activity

bypass assertion violation for parity

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-02-09 16:33:30 -08:00
parent 6b48b25beb
commit 2f86d9de75
2 changed files with 7 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/solver.cpp
View file

@ -1056,7 +1056,9 @@ namespace polysat {
void solver::assign_eval(sat::literal lit) { void solver::assign_eval(sat::literal lit) {
signed_constraint const c = lit2cnstr(lit); signed_constraint const c = lit2cnstr(lit);
LOG_V(10, "Evaluate: " << lit_pp(*this, lit)); LOG_V(10, "Evaluate: " << lit_pp(*this, lit));
if (!c.is_currently_true(*this)) IF_VERBOSE(0, verbose_stream() << c << " is not currently true\n"); if (!c.is_currently_true(*this)) {
IF_VERBOSE(0, verbose_stream() << "\n" << c << " is not currently true\n");
}
SASSERT(c.is_currently_true(*this)); SASSERT(c.is_currently_true(*this));
VERIFY_EQ(c.eval(*this), l_true); VERIFY_EQ(c.eval(*this), l_true);
unsigned level = 0; unsigned level = 0;

5
src/math/polysat/variable_elimination.cpp
View file

@ -696,7 +696,10 @@ namespace polysat {
#else #else
pdd a_pi = s.pseudo_inv(a); pdd a_pi = s.pseudo_inv(a);
//precondition.insert_eval(~s.eq(a_pi * a, rational::power_of_two(a_parity))); // TODO: This is unfortunately not a justification as the inverse might not be set yet (Can we make it to one?) //precondition.insert_eval(~s.eq(a_pi * a, rational::power_of_two(a_parity))); // TODO: This is unfortunately not a justification as the inverse might not be set yet (Can we make it to one?)
precondition.insert_eval(~s.parity_at_most(a, a_parity)); auto c = ~s.parity_at_most(a, a_parity);
if (!c.is_currently_false(s))
return { p, false };
precondition.insert_eval(c);
#endif #endif
pdd shift = a; pdd shift = a;