projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3fe6b54) | patch
Fix assertion failure due to missing clause id (#180)
authorAndres Nötzli <andres.noetzli@gmail.com>
Fri, 23 Jun 2017 06:56:45 +0000 (23:56 -0700)
committerGitHub <noreply@github.com>
Fri, 23 Jun 2017 06:56:45 +0000 (23:56 -0700)
commitea8e9af7e428930898ba42d9a80ad725dee43cc7
tree17a011f5219038cfd80021df9ac18b94910eb641tree
parent3fe6b54ff58533adf84220bb77dbcac31ad5e157commit | diff
Fix assertion failure due to missing clause id (#180)

This commit fixes bug 821. As written in the description of the bug, the issue
is that `id` is not being set on one of the paths in addClause(), specifically
in the case where all but one literal are assigned false and the remaining
literal is assigned true. In that case, we are not actually adding anything and
set the `id` to `ClauseIdUndef`.
src/prop/minisat/core/Solver.cc diff | blob | history
test/regress/regress0/push-pop/Makefile.am diff | blob | history
test/regress/regress0/push-pop/bug821.smt2 [new file with mode: 0644] blob