From af23f226bf6bb909513a8b1f3787e1463a86953d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 11 Aug 2015 09:07:18 +0200 Subject: [PATCH] take 'iff' into account in assertion on transitivity Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 735079350..f9935fba0 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2633,6 +2633,8 @@ proof * ast_manager::mk_transitivity(proof * p1, proof * p2) { tout << mk_pp(to_app(get_fact(p1))->get_decl(), *this) << "\n"; tout << mk_pp(to_app(get_fact(p2))->get_decl(), *this) << "\n";); SASSERT(to_app(get_fact(p1))->get_decl() == to_app(get_fact(p2))->get_decl() || + ((is_iff(get_fact(p1)) || is_eq(get_fact(p1))) && + (is_iff(get_fact(p2)) || is_eq(get_fact(p2)))) || ( (is_eq(get_fact(p1)) || is_oeq(get_fact(p1))) && (is_eq(get_fact(p2)) || is_oeq(get_fact(p2))))); CTRACE("mk_transitivity", to_app(get_fact(p1))->get_arg(1) != to_app(get_fact(p2))->get_arg(0),