File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -439,13 +439,13 @@ bool Checker::propagate_chain (const vector<int64_t> * chain) {
439439 int unit = 0 ;
440440 for (int k = 0 ; k < size; k++)
441441 if (val (lits[k]) >= 0 ) {
442- if (unit) return false ;
442+ if (unit) return true ;
443443 unit = lits[k];
444444 }
445- if (!unit) return true ;
445+ if (!unit) return false ;
446446 assign (unit);
447447 }
448- return false ;
448+ return true ;
449449}
450450
451451bool Checker::check (const vector<int64_t > * chain) {
Original file line number Diff line number Diff line change @@ -158,12 +158,12 @@ core () {
158158 # failed=`expr $failed + 1`
159159 # fi
160160 # fi
161- if $fratchecker -l $prf
161+ if $fratchecker elab $prf -s -m $cnf -v
162162 then
163163 echo " ${GOOD} ok${NORMAL} (proof checked)"
164164 ok=` expr $ok + 1`
165165 else
166- echo " ${BAD} FAILED${NORMAL} (proof check '$fratchecker -l $prf ' failed)"
166+ echo " ${BAD} FAILED${NORMAL} (proof check '$fratchecker elab $prf -s -m $cnf -v ' failed)"
167167 failed=` expr $failed + 1`
168168 fi
169169 else
You can’t perform that action at this time.
0 commit comments