luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

glucose2: Don't try to justify toplevel assignments 

Doing so isn't necessary and would occasionally result in violated
assertions within glucose2.
This commit is contained in:
Jannis Harder 2024-09-07 13:16:20 +02:00
parent d1aa15b0c8
commit d9b5bf65e8
1 changed files with 1 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/sat/glucose2/CGlucoseCore.h
View File

@ -94,6 +94,7 @@ inline Lit Solver::pickJustLit( int& index ){
for( ; jhead < trail.size() ; jhead++ ){ for( ; jhead < trail.size() ; jhead++ ){
Var x = var(trail[jhead]); Var x = var(trail[jhead]);
if( !decisionLevel() && !isRoundWatch(x) ) continue; if( !decisionLevel() && !isRoundWatch(x) ) continue;
if( level(x) == 0 ) continue;
if( isJReason(x) && l_Undef == value( getFaninVar0(x) ) && l_Undef == value( getFaninVar1(x) ) ) if( isJReason(x) && l_Undef == value( getFaninVar0(x) ) && l_Undef == value( getFaninVar1(x) ) )
pushJustQueue(x,jhead); pushJustQueue(x,jhead);
} }