fix #4120

NikolajBjorner · NikolajBjorner · commit 8996e8129e4d · 2020-04-27T12:06:33.000-07:00
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;

Original file line number	Diff line number	Diff line change
`@@ -27,6 +27,8 @@ br_status recfun_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr *`
`27`	`27`	`return BR_FAILED;`
`28`	`28`	`}`
`29`	`29`	`recfun::def const& d = m_rec.get_def(f);`
	`30`	`+ if (!d.get_rhs())`
	`31`	`+ return BR_FAILED;`
`30`	`32`	`var_subst sub(m);`
`31`	`33`	`result = sub(d.get_rhs(), num_args, args);`
`32`	`34`	`return BR_REWRITE_FULL;`