1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
|
Description: 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.
Author: Fabian Wolff <fabi.wolff@arcor.de>
Forwarded: no
Last-Update: 2020-08-30
---
This patch header follows DEP-3: http://dep.debian.net/deps/dep3/
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2132,38 +2132,38 @@
regress3/bmc-ibm-2.smtv1.smt2
regress3/bmc-ibm-5.smtv1.smt2
regress3/bmc-ibm-7.smtv1.smt2
- regress3/bv_to_int_and_or.smt2
regress3/eq_diamond14.smtv1.smt2
regress3/friedman_n6_i4.smtv1.smt2
regress3/hole9.cvc
regress3/incorrect1.smtv1.smt2
- regress3/issue2429.smt2
regress3/issue4170.smt2
- regress3/pp-regfile.smtv1.smt2
regress3/qwh.35.405.shuffled-as.sat03-1651.smtv1.smt2
- regress3/siegel-nl-bases.smt2
regress3/sixfuncs.sy
regress3/strings-any-term.sy
regress3/strings/extf_d_perf.smt2
- regress3/strings/unsat-circ-reduce.smt2
)
#-----------------------------------------------------------------------------#
# Regression level 4 tests
set(regress_4_tests
- regress4/C880mul.miter.shuffled-as.sat03-348.smtv1.smt2
regress4/NEQ016_size5.smtv1.smt2
- regress4/bug143.smtv1.smt2
- regress4/comb2.shuffled-as.sat03-420.smtv1.smt2
regress4/hole10.cvc
- regress4/instance_1151.smtv1.smt2
)
#-----------------------------------------------------------------------------#
# Disabled tests, will not be run.
set(regression_disabled_tests
+ regress3/bv_to_int_and_or.smt2
+ regress3/issue2429.smt2
+ regress3/pp-regfile.smtv1.smt2
+ regress3/siegel-nl-bases.smt2
+ regress3/strings/unsat-circ-reduce.smt2
+ regress4/C880mul.miter.shuffled-as.sat03-348.smtv1.smt2
+ regress4/bug143.smtv1.smt2
+ regress4/comb2.shuffled-as.sat03-420.smtv1.smt2
+ regress4/instance_1151.smtv1.smt2
regress0/arith/bug549.cvc
regress0/arith/incorrect1.smtv1.smt2
regress0/arith/integers/arith-int-014.cvc
--- a/test/system/CMakeLists.txt
+++ b/test/system/CMakeLists.txt
@@ -26,11 +26,11 @@
add_dependencies(build-systemtests ${name})
endmacro()
-cvc4_add_system_test(boilerplate)
-cvc4_add_system_test(ouroborous)
-cvc4_add_system_test(reset_assertions)
-cvc4_add_system_test(sep_log_api)
-cvc4_add_system_test(smt2_compliance)
-cvc4_add_system_test(statistics)
-cvc4_add_system_test(two_smt_engines)
+# cvc4_add_system_test(boilerplate)
+# cvc4_add_system_test(ouroborous)
+# cvc4_add_system_test(reset_assertions)
+# cvc4_add_system_test(sep_log_api)
+# cvc4_add_system_test(smt2_compliance)
+# cvc4_add_system_test(statistics)
+# cvc4_add_system_test(two_smt_engines)
# TODO: Move CVC4JavaTest.java to test/java and delete run_java_test (after full cmake migration)
|
