From 8a85cfdb128b1426c3e6bb5be20dc987e64a2e37 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 30 Sep 2021 09:32:04 -0700 Subject: [PATCH] fix #5579 - It is only possible to reach this case when new assertions are created. --- src/smt/theory_special_relations.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index 4a8070927..78d5984e5 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -325,14 +325,12 @@ namespace smt { ); continue; } - expr_ref f_app(m.mk_app(f, arg1, arg2), m); + expr_ref f_app(m.mk_app(f, arg1, arg2), m); ensure_enode(f_app); literal f_lit = ctx.get_literal(f_app); switch (ctx.get_assignment(f_lit)) { case l_true: - UNREACHABLE(); - // it should already be the case that v1 and reach v2 in the graph. - // whenever f(n1, n2) is asserted. + SASSERT(new_assertion); break; case l_false: { //