projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1c0a94f) | patch
Make strings emp inference an unhandled inference for proofs (#6575)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 19 May 2021 21:33:06 +0000 (16:33 -0500)
committerGitHub <noreply@github.com>
Wed, 19 May 2021 21:33:06 +0000 (21:33 +0000)
commit081f3676865215c88d057b7d5d832e24e3c263bb
tree71cb90546d6ac4acdf4eb5d3d4104ad03ef5ddd9tree
parent1c0a94f3797c0746c760009975012cfd0a247583commit | diff
Make strings emp inference an unhandled inference for proofs (#6575)

The strings inference id STRINGS_INFER_EMP is a rare inference that currently leads to a segfault when proof reconstruction is tried for it. This PR makes it unhandled.

This was caught by a new regression on the soon-to-be-merged jh-new branch.
src/theory/strings/infer_proof_cons.cpp diff | blob | history