From 77e7dcb3c30e78231e3e5a3f882495e8162a2169 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 Apr 2020 16:32:57 -0700 Subject: [PATCH] fix #3874 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 7e4607e1c..cb528a7fe 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2915,10 +2915,8 @@ proof * ast_manager::mk_transitivity(proof * p1, proof * p2) { // OEQ is compatible with EQ for transitivity. func_decl* f = to_app(get_fact(p1))->get_decl(); if (is_oeq(get_fact(p2))) f = to_app(get_fact(p2))->get_decl(); - proof* p = mk_app(m_basic_family_id, PR_TRANSITIVITY, p1, p2, mk_app(f, to_app(get_fact(p1))->get_arg(0), to_app(get_fact(p2))->get_arg(1))); + return mk_app(m_basic_family_id, PR_TRANSITIVITY, p1, p2, mk_app(f, to_app(get_fact(p1))->get_arg(0), to_app(get_fact(p2))->get_arg(1))); -// SASSERT(p->get_id() != 202); - return p; } proof * ast_manager::mk_transitivity(proof * p1, proof * p2, proof * p3) { @@ -2961,7 +2959,6 @@ proof * ast_manager::mk_monotonicity(func_decl * R, app * f1, app * f2, unsigned args.append(num_proofs, (expr**) proofs); args.push_back(mk_app(R, f1, f2)); proof* p = mk_app(m_basic_family_id, PR_MONOTONICITY, args.size(), args.c_ptr()); - SASSERT(p->get_id() != 202); return p; }