10
10
11
11
package org .sosy_lab .java_smt .test ;
12
12
13
+ import static org .junit .Assert .assertThrows ;
14
+
13
15
import org .junit .Before ;
14
16
import org .junit .Test ;
15
17
import org .sosy_lab .java_smt .api .BooleanFormula ;
@@ -30,35 +32,39 @@ public void validLogicTest() throws SolverException, InterruptedException {
30
32
assertThatFormula (expected ).isEquivalentTo (broken );
31
33
}
32
34
33
- @ Test ( expected = IllegalArgumentException . class )
34
- public void wrongLogicTest () throws SolverException , InterruptedException {
35
+ @ Test
36
+ public void wrongLogicTest () {
35
37
// When we change the code to not use sanitize() solver seem to just ignore set-logic
36
38
// Except for OpenSMT, which always crashes
37
- BooleanFormula expected = mgr .parse ("(declare-const v Int)(assert (= v 3))" );
38
- BooleanFormula broken =
39
- mgr .parse ("(set-logic QF_UF)" + "(declare-const v Int)" + "(assert (= v 3))" );
40
- assertThatFormula (expected ).isEquivalentTo (broken );
39
+ assertThrows (
40
+ IllegalArgumentException .class ,
41
+ () -> mgr .parse ("(set-logic QF_UF)" + "(declare-const v Int)" + "(assert (= v 3))" ));
41
42
}
42
43
43
- @ Test ( expected = IllegalArgumentException . class )
44
- public void logicAfterOptionTest () throws SolverException , InterruptedException {
44
+ @ Test
45
+ public void logicAfterOptionTest () {
45
46
BooleanFormula expected = mgr .parse ("(declare-const v Int)(assert (= v 3))" );
46
- BooleanFormula broken =
47
- mgr .parse (
48
- "(set-option :produce-models true)"
49
- + "(set-logic ALL)"
50
- + "(declare-const v Int)"
51
- + "(assert (= v 3))" );
52
- assertThatFormula (expected ).isEquivalentTo (broken );
47
+ assertThrows (
48
+ IllegalArgumentException .class ,
49
+ () ->
50
+ mgr .parse (
51
+ "(set-option :produce-models true)"
52
+ + "(set-logic ALL)"
53
+ + "(declare-const v Int)"
54
+ + "(assert (= v 3))" ));
53
55
}
54
56
55
- @ Test ( expected = IllegalArgumentException . class )
56
- public void logicUsedTwiceTest () throws SolverException , InterruptedException {
57
+ @ Test
58
+ public void logicUsedTwiceTest () {
57
59
BooleanFormula expected = mgr .parse ("(declare-const v Int)(assert (= v 3))" );
58
- BooleanFormula broken =
59
- mgr .parse (
60
- "(set-logic ALL)" + "(declare-const v Int)" + "(set-logic QF_UF)" + "(assert (= v 3))" );
61
- assertThatFormula (expected ).isEquivalentTo (broken );
60
+ assertThrows (
61
+ IllegalArgumentException .class ,
62
+ () ->
63
+ mgr .parse (
64
+ "(set-logic ALL)"
65
+ + "(declare-const v Int)"
66
+ + "(set-logic QF_UF)"
67
+ + "(assert (= v 3))" ));
62
68
}
63
69
64
70
@ Test
@@ -68,12 +74,13 @@ public void exitAtTheEnd() throws SolverException, InterruptedException {
68
74
assertThatFormula (expected ).isEquivalentTo (broken );
69
75
}
70
76
71
- @ Test (expected = IllegalArgumentException .class )
72
- public void exitNotTheEnd () throws SolverException , InterruptedException {
73
- BooleanFormula expected = mgr .parse ("(declare-const v Int)(assert (= v 3))" );
74
- BooleanFormula broken =
75
- mgr .parse ("(declare-const v Int)" + "(assert (= v 3))" + "(exit)" + "(assert (= v 0))" );
76
- assertThatFormula (expected ).isEquivalentTo (broken );
77
+ @ Test
78
+ public void exitNotTheEnd () {
79
+ assertThrows (
80
+ IllegalArgumentException .class ,
81
+ () ->
82
+ mgr .parse (
83
+ "(declare-const v Int)" + "(assert (= v 3))" + "(exit)" + "(assert (= v 0))" ));
77
84
}
78
85
79
86
@ Test
@@ -130,8 +137,6 @@ public void globalStackResetAssertionsTest() throws SolverException, Interrupted
130
137
131
138
@ Test
132
139
public void stackResetTest () throws SolverException , InterruptedException {
133
- requireParser ();
134
- requireIntegers ();
135
140
BooleanFormula expected = mgr .parse ("(declare-const v Int)(assert (= v 3))" );
136
141
BooleanFormula broken =
137
142
mgr .parse (
0 commit comments