mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #5378

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-07-06 00:04:16 +02:00
parent e5aa02b8f5
commit 2a8d00d815
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_recfun.cpp
View file

@ -282,12 +282,14 @@ namespace smt {
auto & vars = e.m_def->get_vars(); auto & vars = e.m_def->get_vars();
expr_ref lhs(e.m_lhs, m); expr_ref lhs(e.m_lhs, m);
unsigned depth = get_depth(e.m_lhs); unsigned depth = get_depth(e.m_lhs);
expr_ref rhs(apply_args(depth, vars, e.m_args, e.m_def->get_rhs()), m); expr_ref rhs(apply_args(depth, vars, e.m_args, e.m_def->get_rhs()), m);
literal lit = mk_eq_lit(lhs, rhs); literal lit = mk_eq_lit(lhs, rhs);
std::function<literal(void)> fn = [&]() { return lit; }; std::function<literal(void)> fn = [&]() { return lit; };
scoped_trace_stream _tr(*this, fn); scoped_trace_stream _tr(*this, fn);
ctx.mk_th_axiom(get_id(), 1, &lit); ctx.mk_th_axiom(get_id(), 1, &lit);
TRACEFN("macro expansion yields " << pp_lit(ctx, lit)); TRACEFN("macro expansion yields " << pp_lit(ctx, lit));
if (has_quantifiers(rhs))
throw default_exception("quantified formulas in recursive functions are not supported");
} }
/** /**
@ -392,6 +394,8 @@ namespace smt {
std::function<literal_vector(void)> fn = [&]() { return clause; }; std::function<literal_vector(void)> fn = [&]() { return clause; };
scoped_trace_stream _tr(*this, fn); scoped_trace_stream _tr(*this, fn);
ctx.mk_th_axiom(get_id(), clause); ctx.mk_th_axiom(get_id(), clause);
if (has_quantifiers(rhs))
throw default_exception("quantified formulas in recursive functions are not supported");
} }
final_check_status theory_recfun::final_check_eh() { final_check_status theory_recfun::final_check_eh() {