projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e9408ca) | patch
Fix open proof for factoring lemma (#5885)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 10 Feb 2021 16:27:44 +0000 (10:27 -0600)
committerGitHub <noreply@github.com>
Wed, 10 Feb 2021 16:27:44 +0000 (10:27 -0600)
commitb6df05346a3bd8c1c68ef74635711ff3e6bd5791
tree19d7fc01ebe2435cc3bbdc9756e01e55bd143e3ctree
parente9408ca21267616bb799ef5f7fda85a1fee9c07ccommit | diff
Fix open proof for factoring lemma (#5885)

We need to add to the current proof, regardless of whether we have used the factor skolem previously.

Fixes bugs found by @HanielB on SMT-LIB runs.
src/theory/arith/nl/ext/factoring_check.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/nl/ufnia-factor-open-proof.smt2 [new file with mode: 0644] blob