projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: af93047) | patch
Clear obsolete pending lemmas in arithmetic (#8236)
authorGereon Kremer <gkremer@cs.stanford.edu>
Wed, 9 Mar 2022 16:37:13 +0000 (17:37 +0100)
committerGitHub <noreply@github.com>
Wed, 9 Mar 2022 16:37:13 +0000 (16:37 +0000)
commitaba33913501586fc695e0a8be4169b962877edfc
tree6f8f3db8fdf534ca3c368b2794ef994f03725d0btree
parentaf930471df9bfe02d8848e1dc1a1eda47dbe8cbecommit | diff
Clear obsolete pending lemmas in arithmetic (#8236)

Arithmetic generally generates nonlinear lemmas as full effort checks, but only sends them out in the subsequent last call effort check. If this one does not happen, the next full effort check still has pending lemmas that may not only be irrelevant now, but possibly carry proofs that are already out of scope.
This PR makes sure that such lemmas are always pruned.
Fixes cvc5/cvc5-projects#465
src/theory/arith/theory_arith.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/nl/proj-issue-465-asan-proofs.smt2 [new file with mode: 0644] blob
test/regress/regress0/use_approx/specsharp-WindowsCard.15.RTE.Terminate_System.Int32_approx.smt2 diff | blob | history
test/regress/regress1/nl/arrowsmith-050317.smt2 diff | blob | history
test/unit/api/cpp/theory_arith_nl_black.cpp diff | blob | history