From 30e8330907cd3eaba47bdb88cdab33d1333553cb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 15 Jul 2023 17:03:44 -0700 Subject: [PATCH] fix #6813 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index f1db92a57..e2e01bbee 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2926,7 +2926,7 @@ proof * ast_manager::mk_transitivity(proof * p1, proof * p2) { if (is_not(fact1->get_arg(1), e) && is_not(e, e) && e == fact2->get_arg(0)) p1 = mk_transitivity(p1, mk_rewrite(fact1->get_arg(1), fact2->get_arg(0))); else if (is_not(fact2->get_arg(0), e) && is_not(e, e) && e == fact1->get_arg(1)) - p2 = mk_transitivity(p1, mk_rewrite(fact1->get_arg(1), fact2->get_arg(0))); + p1 = mk_transitivity(p1, mk_rewrite(fact1->get_arg(1), fact2->get_arg(0))); else { SASSERT(fact1->get_arg(1) == fact2->get_arg(0)); }