mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

fix #3437

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-22 12:24:30 -07:00
parent 077024f024
commit 94234aef97
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_arith_eq.h
View file

@ -40,8 +40,8 @@ namespace smt {
SASSERT(is_fixed(v)); SASSERT(is_fixed(v));
// WARNINING: it is not safe to use get_value(v) here, since // WARNINING: it is not safe to use get_value(v) here, since
// get_value(v) may not satisfy v bounds at this point. // get_value(v) may not satisfy v bounds at this point.
CTRACE("arith_bug", !lower_bound(v).is_rational(), display_var(tout, v);); if (!lower_bound(v).is_rational())
SASSERT(lower_bound(v).is_rational()); return;
numeral const & val = lower_bound(v).get_rational(); numeral const & val = lower_bound(v).get_rational();
value_sort_pair key(val, is_int_src(v)); value_sort_pair key(val, is_int_src(v));
TRACE("arith_eq", tout << mk_pp(get_enode(v)->get_owner(), get_manager()) << " = " << val << "\n";); TRACE("arith_eq", tout << mk_pp(get_enode(v)->get_owner(), get_manager()) << " = " << val << "\n";);