Package: cvc4 / 1.8-2

Metadata

Package Version Patches format
cvc4 1.8-2 3.0 (quilt)

Patch series

view the series file
Patch File delta Description
00 timestamps.patch | (download)

src/base/configuration.cpp | 2 1 + 1 - 0 !
1 file changed, 1 insertion(+), 1 deletion(-)

 make timestamps reproducible
01 disable tests.patch | (download)

test/regress/CMakeLists.txt | 18 9 + 9 - 0 !
test/system/CMakeLists.txt | 14 7 + 7 - 0 !
2 files changed, 16 insertions(+), 16 deletions(-)

 disable some test cases
 The regress* test cases disabled by this patch are absurdly large and
 significantly slow down the build. They may be valuable for the
 upstream developers, but I think for Debian's purposes, the
 functionality of CVC4 is sufficiently tested by the other >2000 test
 cases (especially since we're packaging an official release, which
 has hopefully already been thoroughly tested before). Additionally,
 the system* test cases don't work, not because of a functional
 failure of CVC4, but because there is some error in their setup, so
 this patch disables them as well.
02 install lib dir.patch | (download)

CMakeLists.txt | 3 1 + 2 - 0 !
1 file changed, 1 insertion(+), 2 deletions(-)

 libraries should be installed into $(cmake_install_libdir)
03 remove build path.patch | (download)

src/expr/CMakeLists.txt | 10 10 + 0 - 0 !
src/expr/expr_manager_template.cpp | 2 1 + 1 - 0 !
src/expr/expr_manager_template.h | 2 1 + 1 - 0 !
src/expr/expr_template.cpp | 2 1 + 1 - 0 !
src/expr/expr_template.h | 4 2 + 2 - 0 !
src/expr/kind_template.cpp | 6 3 + 3 - 0 !
src/expr/kind_template.h | 4 2 + 2 - 0 !
src/expr/metakind_template.h | 2 1 + 1 - 0 !
src/expr/mkexpr | 33 16 + 17 - 0 !
src/expr/mkkind | 33 16 + 17 - 0 !
src/expr/mkmetakind | 17 8 + 9 - 0 !
src/expr/type_checker_template.cpp | 8 4 + 4 - 0 !
src/expr/type_properties_template.h | 16 8 + 8 - 0 !
13 files changed, 73 insertions(+), 66 deletions(-)

 remove build path from generated header files
04 spelling errors.patch | (download)

proofs/signatures/drat.plf | 2 1 + 1 - 0 !
proofs/signatures/lrat.plf | 12 6 + 6 - 0 !
proofs/signatures/th_lira.plf | 4 2 + 2 - 0 !
src/api/cvc4cpp.cpp | 8 4 + 4 - 0 !
src/parser/cvc/Cvc.g | 2 1 + 1 - 0 !
src/prop/bvminisat/simp/SimpSolver.cc | 2 1 + 1 - 0 !
src/prop/bvminisat/simp/SimpSolver.h | 2 1 + 1 - 0 !
src/prop/minisat/simp/SimpSolver.cc | 2 1 + 1 - 0 !
src/prop/minisat/simp/SimpSolver.h | 2 1 + 1 - 0 !
src/smt/smt_engine.cpp | 2 1 + 1 - 0 !
src/smt/smt_engine.h | 2 1 + 1 - 0 !
src/theory/arith/theory_arith_private.cpp | 2 1 + 1 - 0 !
src/theory/example/ecdata.h | 2 1 + 1 - 0 !
src/theory/example/theory_uf_tim.h | 2 1 + 1 - 0 !
src/theory/quantifiers_engine.cpp | 2 1 + 1 - 0 !
src/util/string.cpp | 6 3 + 3 - 0 !
src/util/string.h | 4 2 + 2 - 0 !
17 files changed, 29 insertions(+), 29 deletions(-)

 fix spelling errors found by lintian
05 fix headers.patch | (download)

src/fix-install-headers.sh | 3 2 + 1 - 0 !
1 file changed, 2 insertions(+), 1 deletion(-)

 the fix-install-headers.sh script doesn't work with destdir
06 disable tests.patch | (download)

test/regress/CMakeLists.txt | 112 56 + 56 - 0 !
1 file changed, 56 insertions(+), 56 deletions(-)

 disable several failing test cases for now