|
8 | 8 |
|
9 | 9 | package org.sosy_lab.java_smt.test;
|
10 | 10 |
|
11 |
| -import static com.google.common.collect.Iterables.filter; |
12 | 11 | import static com.google.common.collect.Iterables.getLast;
|
13 | 12 | import static com.google.common.truth.Truth.assertThat;
|
14 | 13 | import static com.google.common.truth.Truth.assertWithMessage;
|
|
19 | 18 | import com.google.common.collect.Iterables;
|
20 | 19 | import com.google.common.collect.Multiset;
|
21 | 20 | import com.google.common.truth.TruthJUnit;
|
22 |
| -import java.util.List; |
23 | 21 | import java.util.function.Supplier;
|
24 | 22 | import org.junit.Test;
|
25 | 23 | import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
|
|
29 | 27 | import org.sosy_lab.java_smt.api.FunctionDeclaration;
|
30 | 28 | import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
|
31 | 29 | import org.sosy_lab.java_smt.api.SolverException;
|
| 30 | +import org.sosy_lab.java_smt.basicimpl.Tokenizer; |
32 | 31 |
|
33 | 32 | @SuppressWarnings("checkstyle:linelength")
|
34 | 33 | public class SolverFormulaIOTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 {
|
@@ -481,19 +480,11 @@ private void checkThatAssertIsInLastLine(String dump) {
|
481 | 480 | // Boolector will fail this anyway since bools are bitvecs for btor
|
482 | 481 | TruthJUnit.assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR);
|
483 | 482 |
|
484 |
| - List<String> lines = Splitter.on('\n').splitToList(dump.trim()); |
485 |
| - String lineUnderTest = getLast(lines); |
486 |
| - |
487 |
| - if (solver == Solvers.OPENSMT) { |
488 |
| - // OpenSMT prints assertions over several lines, so lets find the last SMT-LIB command by |
489 |
| - // heuristic: the last line starting with a plain bracket. |
490 |
| - lineUnderTest = getLast(filter(lines, line -> line.startsWith("("))); |
491 |
| - } |
492 |
| - |
| 483 | + String lastCommand = getLast(Tokenizer.tokenize(dump)); |
493 | 484 | assertWithMessage("last line(s) of <\n" + dump + ">")
|
494 |
| - .that(lineUnderTest) |
| 485 | + .that(lastCommand) |
495 | 486 | .startsWith("(assert ");
|
496 |
| - assertWithMessage("last line(s) of <\n" + dump + ">").that(getLast(lines)).endsWith(")"); |
| 487 | + assertWithMessage("last line(s) of <\n" + dump + ">").that(lastCommand).endsWith(")"); |
497 | 488 | }
|
498 | 489 |
|
499 | 490 | @SuppressWarnings("CheckReturnValue")
|
|
0 commit comments