From 75739fdf7b35e79f6403c5c28c28340c7019ff7f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 6 Dec 2012 08:19:42 -0800 Subject: [PATCH] fixed memory smash Signed-off-by: Leonardo de Moura --- src/ast/rewriter/th_rewriter.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 07ee7698d..29034d396 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -483,10 +483,13 @@ struct th_rewriter_cfg : public default_rewriter_cfg { f = to_app(t1)->get_decl(); return unify_core(to_app(t1), t2, new_t1, new_t2, c, first); } - else { + else if (is_arith_bv_app(t2)) { f = to_app(t2)->get_decl(); return unify_core(to_app(t2), t1, new_t2, new_t1, c, first); } + else { + return false; + } } // Apply transformations of the form