Skip to content

Commit 8032954

Browse files
author
StefanoDalMas
committed
fix tests
Signed-off-by: StefanoDalMas <[email protected]>
1 parent 31a725a commit 8032954

File tree

1 file changed

+4
-5
lines changed

1 file changed

+4
-5
lines changed

dartagnan/src/test/java/com/dat3m/dartagnan/asm/armv8/progress64/AsmProgress64Armv8Test.java

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@
2929
import static com.dat3m.dartagnan.utils.Result.PASS;
3030
import com.dat3m.dartagnan.verification.VerificationTask;
3131
import com.dat3m.dartagnan.verification.solving.AssumeSolver;
32-
import com.dat3m.dartagnan.wmm.Wmm;
32+
import com.dat3m.dartagnan.verification.solving.RefinementSolver;
3333

3434
@RunWith(Parameterized.class)
3535
public class AsmProgress64Armv8Test {
@@ -55,10 +55,9 @@ public static Iterable<Object[]> data() throws IOException {
5555

5656
@Test
5757
public void testAllSolvers() throws Exception {
58-
// TODO : RefinementSolver takes too long to run, we have to investigate this
59-
// try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) {
60-
// assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult());
61-
// }
58+
try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) {
59+
assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult());
60+
}
6261
try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) {
6362
assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult());
6463
}

0 commit comments

Comments
 (0)