projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 29959be) | patch
Enable proof checking for QF_LRA benchmarks (#2928)
authorAndres Noetzli <andres.noetzli@gmail.com>
Tue, 4 Jun 2019 23:37:27 +0000 (16:37 -0700)
committerGitHub <noreply@github.com>
Tue, 4 Jun 2019 23:37:27 +0000 (16:37 -0700)
commit0536a743411b882cda88b18ca21cd5dc29828f54
treee8b41dfbae6d50c9f074ae02ac826d5f6ed8c51dtree
parent29959bec6e023f64cad0a5d43b18052f08ac94c5commit | diff
Enable proof checking for QF_LRA benchmarks (#2928)

Due to issues in the current proof code, this commit also disables proof
checking for five QF_LRA benchmarks (see issue #2855).
12 files changed:
proofs/signatures/CMakeLists.txt diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/logic_info.cpp diff | blob | history
test/regress/regress0/lemmas/sc_init_frame_gap.induction.smt diff | blob | history
test/regress/regress0/uflra/constants0.smt diff | blob | history
test/regress/regress0/uflra/pb_real_10_0200_10_22.smt diff | blob | history
test/regress/regress0/uflra/pb_real_10_0200_10_26.smt diff | blob | history
test/regress/regress1/lemmas/pursuit-safety-8.smt diff | blob | history
test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt diff | blob | history
test/regress/regress2/arith/pursuit-safety-11.smt diff | blob | history
test/regress/regress2/arith/pursuit-safety-12.smt diff | blob | history
test/unit/theory/logic_info_white.h diff | blob | history