mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
parent
4be6927460
commit
e8ef9a85a4
|
@ -134,6 +134,10 @@ namespace {
|
|||
|
||||
void collect_param_descrs(param_descrs & r) override {
|
||||
m_context.collect_param_descrs(r);
|
||||
insert_timeout(r);
|
||||
insert_rlimit(r);
|
||||
insert_max_memory(r);
|
||||
insert_ctrl_c(r);
|
||||
}
|
||||
|
||||
void collect_statistics(statistics & st) const override {
|
||||
|
|
|
@ -1738,6 +1738,7 @@ public:
|
|||
TRACE("arith", /*display(tout);*/
|
||||
ctx().display(tout);
|
||||
);
|
||||
|
||||
switch (check_lia()) {
|
||||
case l_true:
|
||||
break;
|
||||
|
@ -1748,7 +1749,7 @@ public:
|
|||
st = FC_CONTINUE;
|
||||
break;
|
||||
}
|
||||
|
||||
|
||||
switch (check_nla()) {
|
||||
case l_true:
|
||||
break;
|
||||
|
@ -1759,6 +1760,7 @@ public:
|
|||
st = FC_GIVEUP;
|
||||
break;
|
||||
}
|
||||
|
||||
if (delayed_assume_eqs()) {
|
||||
++m_stats.m_assume_eqs;
|
||||
return FC_CONTINUE;
|
||||
|
|
Loading…
Reference in a new issue