(proof-new) Minor fix and allow proof option (#6085)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 9 Mar 2021 19:02:14 +0000 (13:02 -0600)
committerGitHub <noreply@github.com>
Tue, 9 Mar 2021 19:02:14 +0000 (13:02 -0600)
commitb384526f32eab67bce49c26e38d9bd7d8b1baca0
tree1c35fc83c23f11928ef6be32cb493237730568ea
parent1b180f87266ffa206da1d5b772816b80e7f97c14
(proof-new) Minor fix and allow proof option (#6085)

This is in preparation for enabling CI / proofs on master.

This does not throw an option exception when proofs are enabled, it also makes a fix that was missing on master and needed for regressions to pass on master.

This is partially taken from #5980.
src/smt/set_defaults.cpp
src/theory/builtin/proof_checker.cpp