projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 59d9aad) | patch
Do not process conjunctions as facts in strings (#6065)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 8 Mar 2021 09:40:05 +0000 (03:40 -0600)
committerGitHub <noreply@github.com>
Mon, 8 Mar 2021 09:40:05 +0000 (09:40 +0000)
commit85d00e88892a16e63e520c0c1bde713352316b79
treea2971acc08e1a9bd2e2da110fa79b01a03775a1dtree
parent59d9aad4839e64e0f6d6b57ff112c418ffbbe9fbcommit | diff
Do not process conjunctions as facts in strings (#6065)

This changes things so we process inferences with AND conclusions as lemmas always.

This fixes #6056, that benchmark times out.
src/theory/strings/infer_info.cpp diff | blob | history