From da4289fadc378f5cc601abeb5e37176ed16c9b8a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 25 Oct 2016 20:47:48 -0700 Subject: [PATCH] fix unit tests for pb Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/pb2bv_rewriter.cpp | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index 8871c3dd8..0cae3f307 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -140,10 +140,17 @@ struct pb2bv_rewriter::imp { case l_true: return mk_and(fmls); case l_false: - fmls.push_back(bv.mk_ule(bound, es.back())); + if (!es.empty()) { + fmls.push_back(bv.mk_ule(bound, es.back())); + } return mk_or(fmls); case l_undef: - fmls.push_back(m.mk_eq(bound, es.back())); + if (es.empty()) { + fmls.push_back(m.mk_bool_val(k.is_zero())); + } + else { + fmls.push_back(m.mk_eq(bound, es.back())); + } return mk_and(fmls); default: UNREACHABLE();