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 issue #203: domain range was one too large

Browse source 
Signed-off-by: unknown <nbjorner@nikolaj-z.redmond.corp.microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-08-24 15:55:40 -07:00
parent 4ce80f1aed
commit ee5f1ad6b6
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_dl.cpp
View file

@ -235,13 +235,14 @@ namespace smt {
} }
app* mk_bv_constant(uint64 val, sort* s) { 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) { app* max_value(sort* s) {
uint64 sz; uint64 sz;
VERIFY(u().try_get_size(s, 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) { void mk_lt(app* x, app* y) {