Skip to content

Commit d15f5d3

Browse files
committed
Moved TestSMTMod to newsmt2
1 parent de9628d commit d15f5d3

File tree

1 file changed

+6
-1
lines changed

1 file changed

+6
-1
lines changed

key.core/src/test/java/de/uka/ilkd/key/smt/TestSMTMod.java renamed to key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/TestSMTMod.java

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
/* This file is part of KeY - https://key-project.org
22
* KeY is licensed under the GNU General Public License Version 2
33
* SPDX-License-Identifier: GPL-2.0-only */
4-
package de.uka.ilkd.key.smt;
4+
package de.uka.ilkd.key.smt.newsmt2;
55

66
import java.io.File;
77

@@ -10,6 +10,10 @@
1010
import de.uka.ilkd.key.proof.Goal;
1111
import de.uka.ilkd.key.proof.Proof;
1212
import de.uka.ilkd.key.proof.io.ProblemLoaderException;
13+
import de.uka.ilkd.key.smt.SMTProblem;
14+
import de.uka.ilkd.key.smt.SMTSolverResult;
15+
import de.uka.ilkd.key.smt.SMTTestSettings;
16+
import de.uka.ilkd.key.smt.SolverLauncher;
1317
import de.uka.ilkd.key.smt.solvertypes.SolverType;
1418
import de.uka.ilkd.key.smt.solvertypes.SolverTypeImplementation;
1519
import de.uka.ilkd.key.smt.solvertypes.SolverTypes;
@@ -46,6 +50,7 @@ public class TestSMTMod {
4650
/**
4751
* This tests if x mod y is non-negative and x mod y < |y| for y != 0
4852
* thus satisfying the definition of euclidean modulo
53+
* Tests for Z3 and CVC4
4954
*
5055
* @throws ProblemLoaderException Occured Exception during load of problem file
5156
*/

0 commit comments

Comments
 (0)