Fallback for sequential substitution proof reconstruction (#8730)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 6 May 2022 22:36:04 +0000 (17:36 -0500)
committerGitHub <noreply@github.com>
Fri, 6 May 2022 22:36:04 +0000 (22:36 +0000)
commit88f1d4e1b1ae8c7b320ec357fb02fdecbc096f7b
treeff3d69ffb1c6be399247ea6b7e84a4782596aecb
parent15812533fce5ae7f2c1d1961c19c8f440c818274
Fallback for sequential substitution proof reconstruction (#8730)

This makes our proof reconstruction fallback to a trivial sequential reconstruction in very rare cases where a sequential substitution fails to reconstruct. This can happen in some rare cases where terms are used in the domain of a substitution that otherwise would be modified by earlier substitutions. This occurs on 2 QF_SLIA benchmarks, attached is a delta-debugged version.

This also changes a warning message to a trace for this case, as a warning message may cause LFSC proof checking to fail when it should just give a warning for a TRUST_SUBS step, which is the default behavior regardless.
src/smt/proof_post_processor.cpp
test/regress/cli/CMakeLists.txt
test/regress/cli/regress2/strings/dd.trust-subs.smt2 [new file with mode: 0644]