mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

fix #3019

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-15 21:40:52 -10:00
parent 839d6fd5be
commit 1da64bfe4c
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/subpaving/subpaving_t_def.h
View file

@ -1777,6 +1777,8 @@ void context_t<C>::assert_units(node * n) {
ineq * a = UNTAG(ineq*, *it);
bool axiom = GET_TAG(*it) != 0;
TRACE("subpaving_init", tout << "asserting: "; display(tout, a); tout << ", axiom: " << axiom << "\n";);
if (a->x() == null_var)
continue;
propagate_bound(a->x(), a->value(), a->is_lower(), a->is_open(), n, justification(axiom));
if (inconsistent(n))
break;