mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #5255

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-05-09 20:48:11 -07:00
parent 31a5bd7fd7
commit 28328e63fd
1 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/tactic/arith/pb2bv_tactic.cpp
View file

@ -657,13 +657,14 @@ private:
SASSERT(pos); SASSERT(pos);
r = m.mk_true(); r = m.mk_true();
} }
else { else if ((c.is_zero() && k == GE) ||
SASSERT((c.is_zero() && k == GE) || (c.is_one() && k == LE)) {
(c.is_one() && k == LE));
// unit 0 >= x, 1 <= x // unit 0 >= x, 1 <= x
SASSERT(pos); SASSERT(pos);
r = mk_unit(rhs, k == GE); r = mk_unit(rhs, k == GE);
} }
else
throw_non_pb(t);
return; return;
} }
throw_non_pb(t); throw_non_pb(t);
@ -985,7 +986,7 @@ private:
void throw_tactic(expr* e) { void throw_tactic(expr* e) {
std::stringstream strm; std::stringstream strm;
strm << "goal is in a fragment unsupported by pb2bv. Offending expression: " << mk_pp(e, m); strm << "goal is in a fragment not supported by pb2bv. Offending expression: " << mk_pp(e, m);
throw tactic_exception(strm.str()); throw tactic_exception(strm.str());
} }
}; };