mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
remove out
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
ec57d3b15c
commit
e3c35840bb
|
@ -190,7 +190,6 @@ void asserted_formulas::push_scope() {
|
||||||
}
|
}
|
||||||
|
|
||||||
void asserted_formulas::push_scope_core() {
|
void asserted_formulas::push_scope_core() {
|
||||||
std::cout << "push\n";
|
|
||||||
reduce();
|
reduce();
|
||||||
commit();
|
commit();
|
||||||
SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.limit().is_canceled());
|
SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.limit().is_canceled());
|
||||||
|
@ -261,7 +260,6 @@ bool asserted_formulas::check_well_sorted() const {
|
||||||
}
|
}
|
||||||
|
|
||||||
void asserted_formulas::reduce() {
|
void asserted_formulas::reduce() {
|
||||||
std::cout << "reduce\n";
|
|
||||||
if (inconsistent())
|
if (inconsistent())
|
||||||
return;
|
return;
|
||||||
if (canceled())
|
if (canceled())
|
||||||
|
|
Loading…
Reference in a new issue