mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 10:30:44 +00:00
Code Activity

fix assert

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-03-02 09:01:55 -08:00
parent de6fea95f6
commit d5271df888
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/polysat/solver.cpp
View file

@ -447,7 +447,8 @@ namespace polysat {
*/ */
bool solver::repropagate(sat::literal lit, clause& cl) { bool solver::repropagate(sat::literal lit, clause& cl) {
LOG("Re-propagate " << lit << " in " << cl); LOG("Re-propagate " << lit << " in " << cl);
SASSERT(m_bvars.is_undef(lit)); if (!m_bvars.is_undef(lit))
return false;
SASSERT(cl.size() >= 2); SASSERT(cl.size() >= 2);
unsigned idx = (cl[0] == lit) ? 1 : 0; unsigned idx = (cl[0] == lit) ? 1 : 0;
SASSERT(cl[1 - idx] == lit); SASSERT(cl[1 - idx] == lit);