mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
include recursive functions to models. Issue #898
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
6f68355fbc
commit
854bb2197f
|
@ -228,7 +228,7 @@ public:
|
|||
if (m_inc_timeout == UINT_MAX) {
|
||||
IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 2 (without a timeout)\")\n";);
|
||||
lbool r = m_solver2->check_sat(num_assumptions, assumptions);
|
||||
if (r != l_undef || !use_solver1_when_undef()) {
|
||||
if (r != l_undef || !use_solver1_when_undef() || get_manager().canceled()) {
|
||||
return r;
|
||||
}
|
||||
}
|
||||
|
@ -285,10 +285,9 @@ public:
|
|||
}
|
||||
|
||||
virtual void collect_statistics(statistics & st) const {
|
||||
m_solver2->collect_statistics(st);
|
||||
if (m_use_solver1_results)
|
||||
m_solver1->collect_statistics(st);
|
||||
else
|
||||
m_solver2->collect_statistics(st);
|
||||
}
|
||||
|
||||
virtual void get_unsat_core(ptr_vector<expr> & r) {
|
||||
|
|
|
@ -374,6 +374,11 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
void fill(unsigned sz, T const & elem) {
|
||||
resize(sz);
|
||||
fill(sz, elem);
|
||||
}
|
||||
|
||||
bool contains(T const & elem) const {
|
||||
const_iterator it = begin();
|
||||
const_iterator e = end();
|
||||
|
|
Loading…
Reference in a new issue