diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-28 10:45:19 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-28 15:45:19 +0000 |
| commit | dd850b74cb3ff5ab043ccfa124443791dcbcc0bf (patch) | |
| tree | 782470f8b56ebc2770414746d95927b0524a1e42 /src/smt/smt_solver.h | |
| parent | e2b5b08d732b007caae6059616bb341a58d143e3 (diff) | |
Properly guard proof construction for STRINGS_EXTF_EQ_REW (#7519)
Fixes one of the issues raised in cvc5/cvc5-projects#331, the other involves missing skolem definitions for str.replace_all_re @4tXJ7f .
This properly guards cases of proof reconstruction for STRINGS_EXTF_EQ_REW where an intermediate step in the proof checker inferring something stronger than what it is asked to prove. In particular, substitution+rewriting is more powerful than congruence+rewriting:
s=x => (str.<= t s) ----> (= r "") since (str.<= t "") ----> (= r "")
but additionally:
(str.<= t s) * { s -> x } ----> true, which is possible if s occurs as a subterm of t.
The proof reconstruction for STRINGS_EXTF_EQ_REW is not precise as there are several other aspects that are not covered. After this PR, we properly guard and fail to reconstruct if the above issue arises, so the assertion failure will not throw.
Diffstat (limited to 'src/smt/smt_solver.h')
0 files changed, 0 insertions, 0 deletions