mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
remove print breaking build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
abdd982cea
commit
fbf81c88a2
|
@ -4183,7 +4183,6 @@ namespace smt {
|
||||||
expr* e = m_asserted_formulas.get_formula(i);
|
expr* e = m_asserted_formulas.get_formula(i);
|
||||||
if (is_quantifier(e)) {
|
if (is_quantifier(e)) {
|
||||||
quantifier* q = to_quantifier(e);
|
quantifier* q = to_quantifier(e);
|
||||||
std::cout << mk_pp(q, m) << "\n";
|
|
||||||
if (!m.is_rec_fun_def(q)) continue;
|
if (!m.is_rec_fun_def(q)) continue;
|
||||||
SASSERT(q->get_num_patterns() == 1);
|
SASSERT(q->get_num_patterns() == 1);
|
||||||
expr* fn = to_app(q->get_pattern(0))->get_arg(0);
|
expr* fn = to_app(q->get_pattern(0))->get_arg(0);
|
||||||
|
|
Loading…
Reference in a new issue