From ee5f1ad6b62269624c961c45f44cab46daf904fb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Aug 2015 15:55:40 -0700 Subject: [PATCH] fix issue #203: domain range was one too large Signed-off-by: unknown --- src/smt/theory_dl.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp index fc9138bf6..43ec5682e 100644 --- a/src/smt/theory_dl.cpp +++ b/src/smt/theory_dl.cpp @@ -235,13 +235,14 @@ namespace smt { } app* mk_bv_constant(uint64 val, sort* s) { - return b().mk_numeral(rational(val,rational::ui64()),64); + return b().mk_numeral(rational(val, rational::ui64()), 64); } app* max_value(sort* s) { uint64 sz; VERIFY(u().try_get_size(s, sz)); - return mk_bv_constant(sz, s); + SASSERT(sz > 0); + return mk_bv_constant(sz-1, s); } void mk_lt(app* x, app* y) {