mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

check that model is availble before evaluation, issue #595

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-07-01 09:26:01 -07:00
parent 4c786c5f70
commit 654780bb4b
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/interp/iz3base.cpp
View file

@ -280,6 +280,10 @@ bool iz3base::is_sat(const std::vector<ast> &q, ast &_proof, std::vector<ast> &v
else if(vars.size()) {
model_ref(_m);
s.get_model(_m);
if (!_m.get()) {
SASSERT(l_undef == res);
throw iz3_exception("interpolation cannot proceed without a model");
}
for(unsigned i = 0; i < vars.size(); i++){
expr_ref r(m());
_m.get()->eval(to_expr(vars[i].raw()),r,true);