Skip to content

Commit 13d06f2

Browse files
committed
- removed all define-fun tests, because they didn't even test define-fun and JavaSMT does not support it.
1 parent 22b8d1f commit 13d06f2

File tree

2 files changed

+1
-3
lines changed

2 files changed

+1
-3
lines changed

src/org/sosy_lab/java_smt/test/SMTLIB2ParserInterpreterTest.java

-1
Original file line numberDiff line numberDiff line change
@@ -3145,7 +3145,6 @@ public void testExceptionPush()
31453145

31463146
/*PARSE MODEL TESTS*/
31473147

3148-
31493148
@Test
31503149
public void testLetExpression()
31513150
throws IOException, SolverException, InterruptedException, InvalidConfigurationException {

src/org/sosy_lab/java_smt/test/SMTLIB2StringTest.java

+1-2
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@
2424
import org.sosy_lab.java_smt.api.StringFormula;
2525
import org.sosy_lab.java_smt.basicimpl.Generator;
2626

27-
@SuppressWarnings({"CheckReturnValue", "ReturnValueIgnored","EqualsIncompatibleType"})
27+
@SuppressWarnings({"CheckReturnValue", "ReturnValueIgnored", "EqualsIncompatibleType"})
2828
public class SMTLIB2StringTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 {
2929
@Before
3030
public void setUp() {
@@ -343,7 +343,6 @@ public void testRegexIntersection()
343343

344344
BooleanFormula actualResult = mgr.universalParseFromString(x);
345345

346-
347346
assertThat(
348347
actualResult.equals(
349348
"(str.in_re a (re.inter (str.to_re \"\\Qa\\E\") (str.to_re " + "\"\\Qb\\E\")))"));

0 commit comments

Comments
 (0)