From a1f7676c81f3463b8c100c4928984fbf6ab59101 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Jan 2022 03:10:41 +0100 Subject: [PATCH] remove assertion - literals could be assigned but propagation incomplete Signed-off-by: Nikolaj Bjorner --- src/smt/seq_eq_solver.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp index 8eb3e0c98..7ac82eff7 100644 --- a/src/smt/seq_eq_solver.cpp +++ b/src/smt/seq_eq_solver.cpp @@ -393,8 +393,6 @@ bool theory_seq::split_lengths(dependency* dep, lits.push_back(lit1); lits.push_back(lit2); - SASSERT(!ctx.is_relevant(lit1) || ctx.get_assignment(lit1) == l_true); - SASSERT(!ctx.is_relevant(lit2) || ctx.get_assignment(lit2) == l_true); if (ctx.get_assignment(lit1) != l_true || ctx.get_assignment(lit2) != l_true) { ctx.mark_as_relevant(lit1);