fix #4120

Z3Prover · Apr 27, 2020 · 8996e81 · 8996e81
1 parent 4938ea7
commit 8996e81
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/ast/rewriter/recfun_rewriter.cpp b/src/ast/rewriter/recfun_rewriter.cpp
@@ -27,6 +27,8 @@ br_status recfun_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr *
                 return BR_FAILED;
         }
         recfun::def const& d = m_rec.get_def(f);
+        if (!d.get_rhs())
+            return BR_FAILED;
         var_subst sub(m);
         result = sub(d.get_rhs(), num_args, args);
         return BR_REWRITE_FULL;