mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

remove assertion - literals could be assigned but propagation incomplete

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-01-21 03:10:41 +01:00
parent 007af9cb8a
commit a1f7676c81
1 changed files with 0 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/seq_eq_solver.cpp
View file

@ -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);