mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

fix #3426

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-22 20:48:31 -07:00
parent 19c72ab519
commit f158ab8395
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/qe/qe_mbp.cpp
View file

@ -231,7 +231,8 @@ class mbp::impl {
expr_ref tmp(m); expr_ref tmp(m);
sub(fml, tmp); sub(fml, tmp);
expr_ref val = eval(tmp); expr_ref val = eval(tmp);
SASSERT(m.is_true(val) || m.is_false(val) || m.canceled()); if (!m.is_true(val) && !m.is_false(val))
return false;
fmls.push_back(m.is_true(val) ? tmp : mk_not(m, tmp)); fmls.push_back(m.is_true(val) ? tmp : mk_not(m, tmp));
} }
return found_bool; return found_bool;