From c0919b00196f7ef8ef436693618c83116010e99e Mon Sep 17 00:00:00 2001
From: Tianrui Zheng <tianrui.zheng@huawei.com>
Date: Tue, 19 Nov 2024 11:37:27 +0100
Subject: [PATCH] Fix CI tests

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>
---
 .../com/dat3m/dartagnan/c/C11LFDSTest.java    | 15 ++++++----
 .../com/dat3m/dartagnan/c/VMMLFDSTest.java    | 28 +++++++++++--------
 2 files changed, 27 insertions(+), 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
index 906f18f90d..dedd9fc567 100644
--- 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
index 7db0a3bf28..bd6818f75e 100644
--- 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},
         });
     }