mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

extra propagate

Browse source
This commit is contained in:
Jakob Rath 2022-01-20 17:44:57 +01:00
parent c7a09051fa
commit 0a59387d05
1 changed files with 0 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/mul_ovfl_constraint.cpp
View file

@ -140,7 +140,6 @@ namespace polysat {
clause_ref just = cb.build();
SASSERT(just);
s.add_clause(*just);
s.propagate();
SASSERT(s.m_bvars.is_true(conseq.blit()));
return true;
}