projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6e1ac72) | patch
Reinstantiate support for conjunctions in facts (#4377)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 22 Apr 2020 11:32:06 +0000 (04:32 -0700)
committerGitHub <noreply@github.com>
Wed, 22 Apr 2020 11:32:06 +0000 (06:32 -0500)
commit2a38d482462fdf30376c984e7a82c99d08e75f92
treedb3f24fbdc7bd097091dfced40f9d8a6c29c1e39tree
parent6e1ac7281d5986f3636254988979e9048e5267c4commit | diff
Reinstantiate support for conjunctions in facts (#4377)

Fixes #4376. Commit 6255c0356bd78140a9cf075491c1d4608ac27704 removed
support for conjunctions in the conclusion of facts. However,
`F_ENDPOINT_EMP` generates a conjunction in the conclusion of the
inference if multiple components are inferred to be empty. This commit
reinstantiates support for conjunctions in the conclusion of facts.
src/theory/strings/inference_manager.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/strings/issue4376.smt2 [new file with mode: 0644] blob