mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
recursive function definitions; combine model-building functionality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
50b2389e7f
commit
6fef24edb4
|
@ -329,10 +329,11 @@ namespace smt {
|
|||
sub(q->get_expr(), num_decls, args.c_ptr(), tmp);
|
||||
m_curr_model->eval(tmp, result, true);
|
||||
if (m.is_false(result)) {
|
||||
TRACE("model_checker", tout << tmp << "\nevaluates to:\n" << result << "\n";);
|
||||
add_instance(q, args, 0);
|
||||
return false;
|
||||
}
|
||||
TRACE("model_checker", tout << tmp << "\nevaluates to:\n" << result << "\n";);
|
||||
// if (!m.is_true(result)) is_undef = true;
|
||||
}
|
||||
}
|
||||
return !is_undef;
|
||||
|
|
Loading…
Reference in a new issue