Skip to content

Commit a9701a1

Browse files
committed
Mark performance-varying test as THOROUGH
This test used to be THOROUGH but then seemed to be quick. Changes to the sequence of equations, however, may adversely affect the runtime with MiniSat.
1 parent 7b2a7cf commit a9701a1

File tree

1 file changed

+8
-2
lines changed

1 file changed

+8
-2
lines changed
Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,13 @@
1-
CORE
1+
THOROUGH
22
Test
3-
--function Test.check --unwind 10 --no-unwinding-assertions --max-nondet-string-length 10 --java-assume-inputs-non-null
3+
--function Test.check --unwind 10 --no-unwinding-assertions --max-nondet-string-length 10 --java-assume-inputs-non-null --sat-solver cadical
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$
77
--
8+
--
9+
This test completes in less than 3 seconds with CaDiCaL
10+
--
11+
This test completes in less than 3 seconds with CaDiCaL, but may flip between
12+
seconds and several minutes with MiniSat even just changing the order of
13+
equations.

0 commit comments

Comments
 (0)