projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 286ed8f) | patch
Ensure disequality splits are processed as lemmas (#4380)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 22 Apr 2020 18:32:20 +0000 (13:32 -0500)
committerGitHub <noreply@github.com>
Wed, 22 Apr 2020 18:32:20 +0000 (11:32 -0700)
commitd64143f8aec229a673db1ec7b38d94890134d3f5
tree3a967e221e2e881952b885b7fccfd08f21f1b034tree
parent286ed8f8a3d6aece0469e983e87626a25107608dcommit | diff
Ensure disequality splits are processed as lemmas (#4380)

Fixes #4379. This was caused by a splitting lemma rewriting to a conjunction, being processed as a fact, and having a pending phase requirement sent out assuming the inference was to be processed as a lemma. This forces 2 of the splits in the core solver to be always processed as lemmas.
src/theory/strings/core_solver.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/strings/issue4379.smt2 [new file with mode: 0644] blob