Fix CI tests

Signed-off-by: Tianrui Zheng <[email protected]>
hernanponcedeleon · Nov 19, 2024 · c0919b0 · c0919b0
1 parent 05cd66b
commit c0919b0
Show file tree

Hide file tree

Showing 2 changed files with 27 additions and 16 deletions.
diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11LFDSTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11LFDSTest.java
@@ -10,14 +10,14 @@
 import org.junit.Test;
 import org.junit.runner.RunWith;
 import org.junit.runners.Parameterized;
+import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 
 import java.io.IOException;
 import java.util.Arrays;
 
 import static com.dat3m.dartagnan.configuration.Arch.C11;
 import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath;
-import static com.dat3m.dartagnan.utils.Result.FAIL;
-import static com.dat3m.dartagnan.utils.Result.PASS;
+import static com.dat3m.dartagnan.utils.Result.*;
 import static org.junit.Assert.assertEquals;
 
 @RunWith(Parameterized.class)
@@ -46,15 +46,20 @@ protected Provider<Wmm> getWmmProvider() {
         return Providers.createWmmFromName(() -> "c11");
     }
 
+    @Override
+    protected Provider<Solvers> getSolverProvider() {
+        return () -> Solvers.YICES2;
+    }
+
     @Parameterized.Parameters(name = "{index}: {0}, target={1}")
     public static Iterable<Object[]> data() throws IOException {
         // Commented ones take too long ATM
         return Arrays.asList(new Object[][]{
-                // {"dglm", C11, UNKNOWN},
+                {"dglm", C11, UNKNOWN},
                 {"dglm-CAS-relaxed", C11, FAIL},
-                // {"ms", C11, UNKNOWN},
+                {"ms", C11, UNKNOWN},
                 {"ms-CAS-relaxed", C11, FAIL},
-                // {"treiber", C11, UNKNOWN},
+                {"treiber", C11, UNKNOWN},
                 {"treiber-CAS-relaxed", C11, FAIL},
                 {"chase-lev", C11, PASS},
                 // These have an extra thief that violate the assertion

diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/VMMLFDSTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/VMMLFDSTest.java
@@ -10,12 +10,13 @@
 import org.junit.Test;
 import org.junit.runner.RunWith;
 import org.junit.runners.Parameterized;
+import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 
 import java.io.IOException;
 import java.util.Arrays;
 import java.util.EnumSet;
 
-import static com.dat3m.dartagnan.configuration.Arch.IMM;
+import static com.dat3m.dartagnan.configuration.Arch.C11;
 import static com.dat3m.dartagnan.configuration.Property.*;
 import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath;
 import static com.dat3m.dartagnan.utils.Result.*;
@@ -53,20 +54,25 @@ protected Provider<Wmm> getWmmProvider() {
         return Providers.createWmmFromName(() -> "vmm");
     }
 
+    @Override
+    protected Provider<Solvers> getSolverProvider() {
+        return () -> Solvers.YICES2;
+    }
+
     @Parameterized.Parameters(name = "{index}: {0}, target={1}")
     public static Iterable<Object[]> data() throws IOException {
         return Arrays.asList(new Object[][]{
-                {"dglm", IMM, UNKNOWN},
-                {"dglm-CAS-relaxed", IMM, FAIL},
-                {"ms", IMM, UNKNOWN},
-                {"ms-CAS-relaxed", IMM, FAIL},
-                {"treiber", IMM, UNKNOWN},
-                {"treiber-CAS-relaxed", IMM, FAIL},
-                {"chase-lev", IMM, PASS},
+                {"dglm", C11, UNKNOWN},
+                {"dglm-CAS-relaxed", C11, FAIL},
+                {"ms", C11, UNKNOWN},
+                {"ms-CAS-relaxed", C11, FAIL},
+                {"treiber", C11, UNKNOWN},
+                {"treiber-CAS-relaxed", C11, FAIL},
+                {"chase-lev", C11, PASS},
                 // These have an extra thief that violate the assertion
-                {"chase-lev-fail", IMM, FAIL},
-                {"hash_table", IMM, PASS},
-                {"hash_table-fail", IMM, FAIL},
+                {"chase-lev-fail", C11, FAIL},
+                {"hash_table", C11, PASS},
+                {"hash_table-fail", C11, FAIL},
         });
     }