1
+ /* This file is part of KeY - https://key-project.org
2
+ * KeY is licensed under the GNU General Public License Version 2
3
+ * SPDX-License-Identifier: GPL-2.0-only */
1
4
package de .uka .ilkd .key .smt ;
2
5
6
+ import java .io .File ;
7
+
3
8
import de .uka .ilkd .key .control .DefaultUserInterfaceControl ;
4
9
import de .uka .ilkd .key .control .KeYEnvironment ;
5
10
import de .uka .ilkd .key .proof .Goal ;
8
13
import de .uka .ilkd .key .smt .solvertypes .SolverType ;
9
14
import de .uka .ilkd .key .smt .solvertypes .SolverTypeImplementation ;
10
15
import de .uka .ilkd .key .smt .solvertypes .SolverTypes ;
11
- import org . junit . Test ;
16
+
12
17
import org .key_project .util .helper .FindResources ;
18
+
19
+ import org .junit .Test ;
13
20
import org .slf4j .Logger ;
14
21
import org .slf4j .LoggerFactory ;
15
22
16
-
17
23
import static org .junit .jupiter .api .Assertions .*;
18
24
19
- import java .io .File ;
20
-
21
25
/**
22
26
* This class is for testing the translation of modulo from KeY to SMT
27
+ *
23
28
* @author Nils Buchholz, 2024
24
29
*/
25
30
public class TestSMTMod {
@@ -41,12 +46,13 @@ public class TestSMTMod {
41
46
/**
42
47
* This tests if x mod y is non-negative and x mod y < |y| for y != 0
43
48
* thus satisfying the definition of euclidean modulo
49
+ *
44
50
* @throws ProblemLoaderException Occured Exception during load of problem file
45
51
*/
46
52
@ Test
47
53
public void testModSpec () throws ProblemLoaderException {
48
54
KeYEnvironment <DefaultUserInterfaceControl > env =
49
- KeYEnvironment .load (new File (testCaseDirectory , "smt/modSpec.key" ));
55
+ KeYEnvironment .load (new File (testCaseDirectory , "smt/modSpec.key" ));
50
56
try {
51
57
Proof proof = env .getLoadedProof ();
52
58
assertNotNull (proof );
0 commit comments