projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4b8972f) | patch
Addressed a bug that occurs when proof production is triggered via text flags in...
authorGuy <katz911@gmail.com>
Mon, 20 Jun 2016 21:20:15 +0000 (14:20 -0700)
committerGuy <katz911@gmail.com>
Mon, 20 Jun 2016 21:20:15 +0000 (14:20 -0700)
commita592e0137504c5788084cb8e150f46f109f566d7
tree0816b285c639e0121a1d0a63033ad29bf25b5e35tree
parent4b8972fec229012812bb7edc9e315c2e54f7c059commit | diff
Addressed a bug that occurs when proof production is triggered via text flags in the input.
Separated some initialization into two phases:
1. Those that can be done when the proof compiliation flag is set
2. Those that can be done only when the --proof option is set.
For #2, deferred their execution until the text flags in the input have been processed
src/proof/proof_manager.cpp diff | blob | history
src/proof/theory_proof.cpp diff | blob | history
src/proof/theory_proof.h diff | blob | history
src/smt/smt_engine.cpp diff | blob | history