mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

fix regression in get-consequence on QF_FD

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-09-08 12:43:18 -07:00
parent 80879ce58b
commit 629e981e01
5 changed files with 33 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/tactic/fd_solver/enum2bv_solver.cpp
View file

@ -146,6 +146,7 @@ public:
m_rewriter.flush_side_constraints(bounds);
m_solver->assert_expr(bounds);
// translate enumeration constants to bit-vectors.
for (expr* v : vars) {
func_decl* f = nullptr;
@ -159,12 +160,13 @@ public:
lbool r = m_solver->get_consequences(asms, bvars, consequences);
// translate bit-vector consequences back to enumeration types
for (unsigned i = 0; i < consequences.size(); ++i) {
unsigned i = 0;
for (expr* c : consequences) {
expr* a = nullptr, *b = nullptr, *u = nullptr, *v = nullptr;
func_decl* f;
rational num;
unsigned bvsize;
VERIFY(m.is_implies(consequences[i].get(), a, b));
VERIFY(m.is_implies(c, a, b));
if (m.is_eq(b, u, v) && is_uninterp_const(u) && m_rewriter.bv2enum().find(to_app(u)->get_decl(), f) && bv.is_numeral(v, num, bvsize)) {
SASSERT(num.is_unsigned());
expr_ref head(m);
@ -174,6 +176,7 @@ public:
consequences[i] = m.mk_implies(a, head);
}
}
++i;
}
return r;
}