mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
'na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f90439fdc5
commit
0af249d651
|
@ -2005,11 +2005,6 @@ public:
|
|||
}
|
||||
|
||||
bool can_propagate() {
|
||||
#if 0
|
||||
if (ctx().at_base_level() && has_delayed_constraints()) {
|
||||
// we could add the delayed constraints here directly to the tableau instead of using bounds variables.
|
||||
}
|
||||
#endif
|
||||
return m_asserted_atoms.size() > m_asserted_qhead;
|
||||
}
|
||||
|
||||
|
|
|
@ -93,6 +93,7 @@ class elim_uncnstr_tactic : public tactic {
|
|||
}
|
||||
|
||||
v = m().mk_fresh_const(nullptr, m().get_sort(t));
|
||||
std::cout << mk_pp(t, m()) << " -> " << mk_pp(v, m()) << "\n";
|
||||
TRACE("elim_uncnstr_bug", tout << "eliminating:\n" << mk_ismt2_pp(t, m()) << "\n";);
|
||||
TRACE("elim_uncnstr_bug_ll", tout << "eliminating:\n" << mk_bounded_pp(t, m()) << "\n";);
|
||||
m_fresh_vars.push_back(v);
|
||||
|
|
Loading…
Reference in a new issue