diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-03-02 14:07:36 -0800 |
|---|---|---|
| committer | Alex Ozdemir <aozdemir@hmc.edu> | 2020-03-02 14:06:42 -0800 |
| commit | dadad0593752613dd16058755bd2570f1fad4572 (patch) | |
| tree | d566d9cb0606f703edada41dedb2b07a95706347 | |
| parent | d5a512ff2567390035ae1cac590ea02232ab3abe (diff) | |
format
| -rw-r--r-- | src/proof/sat_proof_implementation.h | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index 8d7ab6151..8c65d42e7 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -285,7 +285,8 @@ bool TSatProof<Solver>::checkResolution(ClauseId id) { typename Solver::TLit var = steps[i].lit; LitSet clause2; createLitSet(steps[i].id, clause2); - if (!resolve<Solver>(var, clause1, clause2, steps[i].sign)) { + if (!resolve<Solver>(var, clause1, clause2, steps[i].sign)) + { validRes = false; break; } |