projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3f0fd45) | patch
Fix linear arithmetic for duplicate lemmas in incremental (#6784)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 24 Jun 2021 11:37:20 +0000 (06:37 -0500)
committerGitHub <noreply@github.com>
Thu, 24 Jun 2021 11:37:20 +0000 (11:37 +0000)
commit4eaef5e472121396ee77023d49b23556ac69b747
treeb103e2171e75fe6fa7157206f9d6588f16999207tree
parent3f0fd456553223a59001a6bcdc714c3b56192787commit | diff
Fix linear arithmetic for duplicate lemmas in incremental (#6784)

The linear arithmetic solver was not robust to cases where a duplicate lemma is emitted. This leads to non-linear arithmetic not being called to check at full effort, leading to potential model soundness issues.

Fixes #6773.
src/theory/arith/theory_arith_private.cpp diff | blob | history
src/theory/arith/theory_arith_private.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/push-pop/issue6773-arith-no-check.smt2 [new file with mode: 0644] blob