From 28328e63fd4d3bc733809a9f386ecccb78fa0163 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 9 May 2021 20:48:11 -0700 Subject: [PATCH] fix #5255 Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/pb2bv_tactic.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index aeda016c7..98724923b 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -657,13 +657,14 @@ private: SASSERT(pos); r = m.mk_true(); } - else { - SASSERT((c.is_zero() && k == GE) || - (c.is_one() && k == LE)); + else if ((c.is_zero() && k == GE) || + (c.is_one() && k == LE)) { // unit 0 >= x, 1 <= x SASSERT(pos); r = mk_unit(rhs, k == GE); } + else + throw_non_pb(t); return; } throw_non_pb(t); @@ -985,7 +986,7 @@ private: void throw_tactic(expr* e) { 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()); } };