[proof] [sat] Fix lost reference to reason when processing redundant literals (#7108)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Wed, 1 Sep 2021 18:31:56 +0000 (15:31 -0300)
committerGitHub <noreply@github.com>
Wed, 1 Sep 2021 18:31:56 +0000 (15:31 -0300)
commit59e73be8a11f5490e0c8cfc4a5e2ab7ed07b352f
treeaaf7a7dee3b75d5891e6f9936a0facf89e6d2186
parent7a3aa7033719b14b34c0334d6956834b850fa9eb
[proof] [sat] Fix lost reference to reason when processing redundant literals (#7108)

Similarly to the issue when explaining literals, it's necassary to save the
reference to the reason for propagating a redundant literal, as adding
explanations that may be added to the SAT solver during the recursive
elimination of redundant literals may change the original reference.
src/prop/sat_proof_manager.cpp
test/regress/CMakeLists.txt
test/regress/regress2/proofs/sat-proof-reloaded-reason.smt2 [new file with mode: 0644]