diff --git a/benchmarks/icse23/algorithms/Makefile b/benchmarks/icse23/algorithms/Makefile
new file mode 100644
index 000000000..e33faa17b
--- /dev/null
+++ b/benchmarks/icse23/algorithms/Makefile
@@ -0,0 +1,44 @@
+SRC_FILES := $(wildcard ./*.c)
+
+CC := clang-11
+
+KLEE_INCL := /icse23/klee/include
+
+GS_INCL := /icse23/GenSym/headers
+
+FLAGS := -emit-llvm -O0 -Xclang -disable-O0-optnone -c
+KLEE_FLAGS := -D KLEE -g -I $(KLEE_INCL)
+GS_FLAGS := -D GENSYM -fno-discard-value-names -S -I $(GS_INCL)
+LLSC_FLAGS := -D LLSC -fno-discard-value-names -S
+
+KLEE_TARGET := $(SRC_FILES:%.c=%.bc)
+
+KLEE_REPLAY_TARGET := $(SRC_FILES:%.c=%-replay)
+
+KLEE_GEN := $(wildcard ./klee-*)
+
+GS_TARGET := $(SRC_FILES:%.c=%.ll)
+
+LLSC_TARGET := $(SRC_FILES:%.c=%_llsc.ll)
+
+all: gensym klee llsc
+
+gensym: $(GS_TARGET)
+klee: $(KLEE_TARGET)
+llsc: $(LLSC_TARGET)
+klee-exe: $(KLEE_REPLAY_TARGET)
+
+$(KLEE_TARGET): %.bc : %.c
+	$(CC) $(KLEE_FLAGS) $(FLAGS) -o $@ $<
+
+$(KLEE_REPLAY_TARGET): %-replay : %.c
+	$(CC) $(KLEE_FLAGS) -o $@ $< -lkleeRuntest
+
+$(GS_TARGET): %.ll : %.c
+	$(CC) $(GS_FLAGS) $(FLAGS) -o $@ $<
+
+$(LLSC_TARGET): %_llsc.ll : %.c
+	$(CC) $(LLSC_FLAGS) $(FLAGS) -o $@ $<
+
+clean:
+	$(RM) -rf $(KLEE_TARGET) $(KLEE_REPLAY_TARGET) $(KLEE_GEN) $(GS_TARGET) $(LLSC_TARGET)
diff --git a/benchmarks/icse23/algorithms/bubblesort.c b/benchmarks/icse23/algorithms/bubblesort.c
new file mode 100644
index 000000000..a18db256c
--- /dev/null
+++ b/benchmarks/icse23/algorithms/bubblesort.c
@@ -0,0 +1,42 @@
+#ifdef KLEE
+#include "klee/klee.h"
+#endif
+#ifdef GENSYM
+#include "gensym_client.h"
+#endif
+
+#define SIZE 6
+
+void bubble_sort(int *d, int n)
+{
+	for (int k = 1; k < n; k++)
+	{
+		for (int i = 1; i < n; i++)
+		{
+			if (d[i] < d[i - 1])
+			{
+				int temp = d[i];
+				d[i] = d[i - 1];
+				d[i - 1] = temp;
+			}
+		}
+	}
+}
+
+int main()
+{
+	int data[SIZE];
+#ifdef KLEE
+  klee_make_symbolic(data, sizeof data, "data");
+#endif
+#ifdef LLSC
+  make_symbolic(data, sizeof(int) * SIZE);
+#endif
+#ifdef GENSYM
+  for (int i = 0; i < SIZE; i++)
+    make_symbolic_whole(data + i, sizeof(int));
+#endif
+
+	bubble_sort(data, SIZE);
+	return 0;
+}
diff --git a/benchmarks/icse23/algorithms/kmpmatcher.c b/benchmarks/icse23/algorithms/kmpmatcher.c
new file mode 100644
index 000000000..2a319906f
--- /dev/null
+++ b/benchmarks/icse23/algorithms/kmpmatcher.c
@@ -0,0 +1,79 @@
+#ifdef KLEE
+#include "klee/klee.h"
+#endif
+#ifdef GENSYM
+#include "gensym_client.h"
+#endif
+
+#define SIZE 10
+
+int pi[10];
+int lt, lp;
+
+void compute_prefix_function(char * P)
+{
+	int q = 0;
+	pi[0] = 0;
+
+	for (int i = 1; i < lp; i++)
+	{
+		while (q > 0 && P[i] != P[q])
+		{
+			q = pi[q - 1];
+		}
+
+		if (P[i] == P[q])
+		{
+			q++;
+		}
+
+		pi[i] = q;
+	}
+}
+
+void KMP_matcher(char * P, char * T)
+{
+	compute_prefix_function(P);
+
+	int q = 0;
+
+	for (int i = 0; i < lt; i++)
+	{
+		while (q > 0 && T[i] != P[q])
+		{
+			q = pi[q - 1];
+		}
+
+		if (T[i] == P[q])
+		{
+			q++;
+		}
+
+		if (q == lp)
+		{
+			printf("matched with shift %d\n", i - lp + 1);
+			q = pi[q - 1];
+		}
+	}
+}
+
+int main()
+{
+  char P[11] = "helloworld";
+	char T[SIZE];
+#ifdef KLEE
+  klee_make_symbolic(T, SIZE, "T");
+#endif
+#ifdef LLSC
+  make_symbolic(T, SIZE);
+#endif
+#ifdef GENSYM
+  make_symbolic(T, SIZE);
+#endif
+	lt = SIZE-1;
+	lp = 10;
+
+	KMP_matcher(P, T);
+
+	return 0;
+}
diff --git a/benchmarks/icse23/algorithms/knapsack.c b/benchmarks/icse23/algorithms/knapsack.c
new file mode 100644
index 000000000..3b25a83f7
--- /dev/null
+++ b/benchmarks/icse23/algorithms/knapsack.c
@@ -0,0 +1,56 @@
+#ifdef KLEE
+#include "klee/klee.h"
+#endif
+#ifdef GENSYM
+#include "gensym_client.h"
+#endif
+
+#include <stdio.h>
+
+#define N 4
+
+int max(int a, int b) { return (a > b) ? a : b; }
+
+int knapSack(int W, int wt[], int val[], int n)
+{
+    // Base Case
+    if (n == 0 || W == 0) return 0;
+
+    // If weight of the nth item is more than
+    // Knapsack capacity W, then this item cannot
+    // be included in the optimal solution
+    if (wt[n - 1] > W)
+        return knapSack(W, wt, val, n - 1);
+
+    // Return the maximum of two cases:
+    // (1) nth item included
+    // (2) not included
+    else
+        return max(
+            val[n - 1]
+                + knapSack(W - wt[n - 1],
+                           wt, val, n - 1),
+            knapSack(W, wt, val, n - 1));
+}
+
+// Driver program to test above function
+int main()
+{
+    //int val[N] = { 60, 100, 120, 130 };
+    int val[N];
+    val[0] = 60; val[1] = 100; val[2] = 120; val[3] = 130;
+    int wt[N];
+#ifdef KLEE
+    klee_make_symbolic(wt, sizeof(int) * N, "wt");
+#endif
+#ifdef LLSC
+    make_symbolic(wt, sizeof(int) * N);
+#endif
+#ifdef GENSYM
+    for (int i = 0; i < N; i++)
+        make_symbolic_whole(wt + i, sizeof(int));
+#endif
+    int W = 50;
+    knapSack(W, wt, val, N);
+    return 0;
+}
diff --git a/benchmarks/icse23/algorithms/mergesort.c b/benchmarks/icse23/algorithms/mergesort.c
new file mode 100644
index 000000000..59bf95981
--- /dev/null
+++ b/benchmarks/icse23/algorithms/mergesort.c
@@ -0,0 +1,95 @@
+#ifdef KLEE
+#include "klee/klee.h"
+#endif
+#ifdef GENSYM
+#include "gensym_client.h"
+#endif
+
+#define SIZE 7
+
+int d[SIZE];
+
+//https://www.geeksforgeeks.org/merge-sort/
+void merge(int arr[], int l, int m, int r)
+{
+    int i, j, k;
+    int n1 = m - l + 1;
+    int n2 = r - m;
+
+    /* create temp arrays */
+    int* L = malloc(n1 * sizeof(int));
+    int* R = malloc(n2 * sizeof(int));
+
+    /* Copy data to temp arrays L[] and R[] */
+    for (i = 0; i < n1; i++)
+        L[i] = arr[l + i];
+    for (j = 0; j < n2; j++)
+        R[j] = arr[m + 1 + j];
+
+    /* Merge the temp arrays back into arr[l..r]*/
+    i = 0; // Initial index of first subarray
+    j = 0; // Initial index of second subarray
+    k = l; // Initial index of merged subarray
+    while (i < n1 && j < n2) {
+        if (L[i] <= R[j]) {
+            arr[k] = L[i];
+            i++;
+        }
+        else {
+            arr[k] = R[j];
+            j++;
+        }
+        k++;
+    }
+
+    /* Copy the remaining elements of L[], if there are any */
+    while (i < n1) {
+        arr[k] = L[i];
+        i++;
+        k++;
+    }
+
+    /* Copy the remaining elements of R[], if there
+    are any */
+    while (j < n2) {
+        arr[k] = R[j];
+        j++;
+        k++;
+    }
+    free(L);
+    free(R);
+}
+
+/* l is for left index and r is right index of the
+sub-array of arr to be sorted */
+void mergeSort(int arr[], int l, int r)
+{
+    if (l < r) {
+        // Same as (l+r)/2, but avoids overflow for
+        // large l and h
+        int m = l + (r - l) / 2;
+
+        // Sort first and second halves
+        mergeSort(arr, l, m);
+        mergeSort(arr, m + 1, r);
+
+        merge(arr, l, m, r);
+    }
+}
+
+int main()
+{
+#ifdef KLEE
+  klee_make_symbolic(d, sizeof d, "data");
+#endif
+#ifdef LLSC
+  make_symbolic(d, sizeof(int) * SIZE);
+#endif
+#ifdef GENSYM
+  for (int i = 0; i < SIZE; i++) {
+    make_symbolic_whole(d+i, sizeof(int));
+  }
+#endif
+  mergeSort(d, 0, SIZE - 1);
+  return 0;
+}
diff --git a/benchmarks/icse23/algorithms/nqueen.c b/benchmarks/icse23/algorithms/nqueen.c
new file mode 100644
index 000000000..a27fbc455
--- /dev/null
+++ b/benchmarks/icse23/algorithms/nqueen.c
@@ -0,0 +1,63 @@
+#ifdef KLEE
+#include "klee/klee.h"
+#endif
+#ifdef GENSYM
+#include "gensym_client.h"
+#endif
+
+// https://www.geeksforgeeks.org/n-queen-problem-backtracking-3/
+#define N 5
+#include <stdbool.h>
+#include <stdio.h>
+
+bool isSafe(int board[N][N], int row, int col) {
+    int i, j;
+    for (i = 0; i < col; i++)
+        if (board[row][i])
+            return false;
+    for (i = row, j = col; i >= 0 && j >= 0; i--, j--)
+        if (board[i][j])
+            return false;
+    for (i = row, j = col; j >= 0 && i < N; i++, j--)
+        if (board[i][j])
+            return false;
+    return true;
+}
+
+bool solveNQUtil(int board[N][N], int col) {
+    if (col >= N) return true;
+    for (int i = 0; i < N; i++) {
+        if (isSafe(board, i, col)) {
+            board[i][col] = 1;
+            if (solveNQUtil(board, col + 1))
+                return true;
+            board[i][col] = 0; // BACKTRACK
+        }
+    }
+    return false;
+}
+
+bool solveNQ() {
+    int board[N][N];
+#ifdef KLEE
+    klee_make_symbolic(board, sizeof(int) * N * N, "board");
+#endif
+#ifdef LLSC
+    make_symbolic(board, sizeof(int) * N * N);
+#endif
+#ifdef GENSYM
+    for (int i = 0; i < N * N; i++)
+        make_symbolic_whole((int*)board + i, sizeof(int));
+#endif
+    if (solveNQUtil(board, 0) == false) {
+        return false;
+    }
+
+    return true;
+}
+
+int main()
+{
+    solveNQ();
+    return 0;
+}
diff --git a/benchmarks/icse23/algorithms/quicksort.c b/benchmarks/icse23/algorithms/quicksort.c
new file mode 100644
index 000000000..62fc4e5f9
--- /dev/null
+++ b/benchmarks/icse23/algorithms/quicksort.c
@@ -0,0 +1,50 @@
+#ifdef KLEE
+#include "klee/klee.h"
+#endif
+#ifdef GENSYM
+#include "gensym_client.h"
+#endif
+
+#define SIZE 7
+
+int d[SIZE];
+
+void qsort(int l, int r)
+{
+	if (l < r)
+	{
+		int x = d[r];
+		int j = l - 1;
+
+		for (int i = l; i <= r; i++)
+		{
+			if (d[i] <= x)
+			{
+				j++;
+				int temp = d[i];
+				d[i] = d[j];
+				d[j] = temp;
+			}
+		}
+
+		qsort(l, j - 1);
+		qsort(j + 1, r);
+	}
+}
+
+int main()
+{
+#ifdef KLEE
+  klee_make_symbolic(d, sizeof d, "data");
+#endif
+#ifdef LLSC
+  make_symbolic(d, sizeof(int) * SIZE);
+#endif
+#ifdef GENSYM
+  for (int i = 0; i < SIZE; i++) {
+    make_symbolic_whole(d+i, sizeof(int));
+  }
+#endif
+	qsort(0, SIZE-1);
+	return 0;
+}
diff --git a/build.sbt b/build.sbt
index 4eeb4e1de..166e540d8 100644
--- a/build.sbt
+++ b/build.sbt
@@ -32,7 +32,7 @@ scalacOptions ++= Seq(
 autoCompilerPlugins := true
 
 //https://www.scala-sbt.org/release/docs/Running-Project-Code.html
-fork := true
+//fork := true
 run / javaOptions ++= Seq(
   "-Xms4G",
   "-Xmx32G",
@@ -60,5 +60,5 @@ lazy val lms = ProjectRef(file("./third-party/lms-clean"), "lms-clean")
 lazy val gensym = (project in file(".")).dependsOn(lms % "test->test; compile->compile")
                                         .configs(Bench)
                                         .settings(inConfig(Bench)(Defaults.testSettings))
-                                        .settings(assembly / mainClass := Some("gensym.RunGenSym"))
-
+                                        .settings(assembly / mainClass := Some("gensym.RunGenSym"),
+                                                  assembly / test := {})
diff --git a/scripts/test_benchmark b/scripts/test_benchmark
index 3f52dde71..2cc823ade 100755
--- a/scripts/test_benchmark
+++ b/scripts/test_benchmark
@@ -66,13 +66,13 @@ echo "[test_benchmark] runtime timeout: $RUNTIME_TIMEOUT"
 if [ "$SCALA_COMPILE" = "true" ] || [ ! -d "gs_gen/${HEAD}" ]; then
 	export SBT_OPTS="-Xms4G -Xmx32G -Xss1024M -XX:MaxMetaspaceSize=8G -XX:ReservedCodeCacheSize=2048M"
 	/usr/bin/time --format "[test_benchmark] scala compilation time => real: %e,\tuser: %U,\tsys: %S" \
-		bloop run sai -m gensym.RunGenSym -- -J-Xms4g -J-Xmx8g -J-Xss1024M -J-XX:MaxMetaspaceSize=8G -J-XX:ReservedCodeCacheSize=2048M ${LL} --use-argv --output=${HEAD} --engine=ImpCPS --main-opt=O0 --entrance=main
+    bloop run sai -m gensym.RunGenSym -- -J-Xms4g -J-Xmx8g -J-Xss1024M -J-XX:MaxMetaspaceSize=8G -J-XX:ReservedCodeCacheSize=2048M ${LL} --use-argv --output=${HEAD} --engine=ImpCPS --main-opt=O0 --entrance=main
 		# sbt "runMain gensym.RunGenSym ${LL} --use-argv --output=${HEAD} --engine=ImpCPS --main-opt=O0 --entrance=main"
 	check_failure "Failed to perform scala compilation with input ${LL}"
 fi
 
 if [ "$CPP_COMPILE" = "true" ] || [ ! -f "gs_gen/${HEAD}/${HEAD}" ]; then
-	( cd gs_gen/${HEAD}; 
+	( cd gs_gen/${HEAD};
 	make clean
 	echo -n "[test_benchmark] "
 	pwd
@@ -109,10 +109,10 @@ if [ "$RUNTIME" = "true" ]; then
 		if [ -z "$SUCCINCT_LOG" ]; then
 			eval "$cmd"
 		else
-			echo "--------------------" >> ${SUCCINCT_LOG}
+      echo "--------------------" >> ${SUCCINCT_LOG}
 			echo "$HEAD $OPT"           >> ${SUCCINCT_LOG}
 			# duplicate to stdout, but write the splitted last line to SUCCINCT_LOG
-			eval "$cmd" | tee >(tail -n 1 | sed 's/#\(blocks\|br\|paths\|threads\|task-in-q\|queries\)/\n&/g' >> ${SUCCINCT_LOG})
+      eval "$cmd" | tee >(tail -n 1 | sed 's/#\(blocks\|br\|paths\|threads\|task-in-q\|queries\)/\n&/g' >> ${SUCCINCT_LOG})
 		fi
 	done
 fi
diff --git a/src/main/scala/gensym/Driver.scala b/src/main/scala/gensym/Driver.scala
index 2c182cad7..104b046dd 100644
--- a/src/main/scala/gensym/Driver.scala
+++ b/src/main/scala/gensym/Driver.scala
@@ -125,7 +125,12 @@ abstract class GenericGSDriver[A: Manifest, B: Manifest]
 
   def makeWithAllCores: Int = {
     val cores = Process("nproc", new File(s"$folder/$appName")).!!.replaceAll("[\\n\\t ]", "").toInt
-    Process(s"make -j$cores", new File(s"$folder/$appName")).!
+    make(cores)
+  }
+
+  def makeWithHalfCores: Int = {
+    val cores = Process("nproc", new File(s"$folder/$appName")).!!.replaceAll("[\\n\\t ]", "").toInt
+    make(cores/2)
   }
 
   // returns the number of paths, obtained by parsing the output
diff --git a/src/main/scala/gensym/RunGenSym.scala b/src/main/scala/gensym/RunGenSym.scala
index 403472cb8..dacdf2665 100644
--- a/src/main/scala/gensym/RunGenSym.scala
+++ b/src/main/scala/gensym/RunGenSym.scala
@@ -1,6 +1,7 @@
 package gensym
 
 import gensym.llvm.parser.Parser._
+import gensym.utils.Utils
 
 case class Config(nSym: Int, useArgv: Boolean, mainFileOpt: String) {
   require(!(nSym > 0 && useArgv))
@@ -70,8 +71,8 @@ object RunGenSym {
     |--emit-block-id-map     - emit a map from block names to id in common.h
     |--emit-var-id-map       - emit a map from variable names to id in common.h
     |--switch-type=<string>  - compilation variants of `switch` statement (default=nonMerge)
-    |  =merge                - only fork `m` paths of distinct targets
-    |  =nonMerge             - fork `n` paths where `n` is the total number of feasible cases (including default)
+    |  =merge                -   only fork `m` paths of distinct targets
+    |  =nonMerge             -   fork `n` paths where `n` is the total number of feasible cases (including default)
     |--help                  - print this help message
     """
 
@@ -83,8 +84,8 @@ object RunGenSym {
       case (options, r"--noOpt") => options + ("optimize" -> false)
       case (options, r"--engine=([a-zA-Z]+)$e") => options + ("engine" -> e)
       case (options, r"--main-opt=O(\d)$n") => options + ("mainOpt" -> ("O"+n))
-      case (options, r"emit-block-id-map") => options + ("blockIdMap" -> true)
-      case (options, r"emit-var-id-map") => options + ("varIdMap" -> true)
+      case (options, r"--emit-block-id-map") => options + ("blockIdMap" -> true)
+      case (options, r"--emit-var-id-map") => options + ("varIdMap" -> true)
       case (options, r"--switch-type=(\w+)$t") => options + ("switchType" -> SwitchType.fromString(t))
       case (options, r"--lib=([-_A-Za-z0-9\/\.]+)$p") => options + ("lib" -> p)
       case (options, "--help") => println(usage.stripMargin); sys.exit(0)
@@ -95,7 +96,7 @@ object RunGenSym {
     val output = options.getOrElse("output", filepath.split("\\/").last.split("\\.")(0)).toString
     val nSym = options.getOrElse("nSym", 0).asInstanceOf[Int]
     val useArgv = options.getOrElse("useArgv", false).asInstanceOf[Boolean]
-    val optimize = options.getOrElse("optimize", Config.opt).asInstanceOf[Boolean]
+    val optimize = options.getOrElse("optimize", true).asInstanceOf[Boolean]
     val engine = options.getOrElse("engine", "ImpCPS").toString
     val mainOpt = options.getOrElse("mainOpt", Config.o0).toString
     val emitBlockIdMap = options.getOrElse("blockIdMap", Config.emitBlockIdMap).asInstanceOf[Boolean]
@@ -120,5 +121,6 @@ object RunGenSym {
     |  nSym=$nSym, useArgv=$useArgv, optimize=$optimize, mainOpt=$mainOpt, switchType=$switchType"""
     println(info.stripMargin)
     gensym.run(parseFile(filepath), output, entrance, Config(nSym, useArgv, mainOpt), libPath)
+    output
   }
 }
diff --git a/src/main/scala/llvm/Benchmarks.scala b/src/main/scala/llvm/Benchmarks.scala
index b3a24823b..926924aa5 100644
--- a/src/main/scala/llvm/Benchmarks.scala
+++ b/src/main/scala/llvm/Benchmarks.scala
@@ -116,22 +116,7 @@ object Benchmarks {
   lazy val argv2Test = parseFile("benchmarks/llvm/argv2.ll")
 
   lazy val unprintableCharTest = parseFile("benchmarks/llvm/unprintable_char.ll")
-  
-  lazy val echo_linked = parseFile("benchmarks/coreutils/echo.ll")
-  lazy val cat_linked = parseFile("benchmarks/coreutils/cat.ll")
-  lazy val true_linked = parseFile("benchmarks/coreutils/true.ll")
-  lazy val false_linked = parseFile("benchmarks/coreutils/false.ll")
-  lazy val base32_linked = parseFile("benchmarks/coreutils/base32.ll")
-  lazy val base64_linked = parseFile("benchmarks/coreutils/base64.ll")
-  lazy val comm_linked = parseFile("benchmarks/coreutils/comm.ll")
-  lazy val cut_linked = parseFile("benchmarks/coreutils/cut.ll")
-  lazy val dirname_linked = parseFile("benchmarks/coreutils/dirname.ll")
-  lazy val expand_linked = parseFile("benchmarks/coreutils/expand.ll")
-  lazy val fold_linked = parseFile("benchmarks/coreutils/fold.ll")
-  lazy val join_linked = parseFile("benchmarks/coreutils/join.ll")
-  lazy val link_linked = parseFile("benchmarks/coreutils/link.ll")
-  lazy val paste_linked = parseFile("benchmarks/coreutils/paste.ll")
-  lazy val pathchk_linked = parseFile("benchmarks/coreutils/pathchk.ll")
+
   lazy val md5sum_linked = parseFile("benchmarks/coreutils/md5sum.ll")
   lazy val sort_linked = parseFile("benchmarks/coreutils/sort.ll")
   lazy val wc_linked = parseFile("benchmarks/coreutils/wc.ll")
@@ -141,6 +126,44 @@ object Benchmarks {
   lazy val true_gs_linked = parseFile("benchmarks/coreutils/true_gs_linked.ll")
 }
 
+object ICSE23CoreutilsPOSIX {
+  val prefix = "/icse23/GenSym/benchmarks/coreutils/gensym_posix"
+  lazy val echo = parseFile(s"$prefix/echo.ll")
+  lazy val cat = parseFile(s"$prefix/cat.ll")
+  lazy val tru = parseFile(s"$prefix/true.ll")
+  lazy val fls = parseFile(s"$prefix/false.ll")
+  lazy val base32 = parseFile(s"$prefix/base32.ll")
+  lazy val base64 = parseFile(s"$prefix/base64.ll")
+  lazy val comm = parseFile(s"$prefix/comm.ll")
+  lazy val cut = parseFile(s"$prefix/cut.ll")
+  lazy val dirname = parseFile(s"$prefix/dirname.ll")
+  lazy val expand = parseFile(s"$prefix/expand.ll")
+  lazy val fold = parseFile(s"$prefix/fold.ll")
+  lazy val join = parseFile(s"$prefix/join.ll")
+  lazy val link = parseFile(s"$prefix/link.ll")
+  lazy val paste = parseFile(s"$prefix/paste.ll")
+  lazy val pathchk = parseFile(s"$prefix/pathchk.ll")
+}
+
+object ICSE23CoreutilsUClibc {
+  val prefix = "/icse23/GenSym/benchmarks/coreutils/gensym_uclibc"
+  lazy val echo = parseFile(s"$prefix/echo.ll")
+  lazy val cat = parseFile(s"$prefix/cat.ll")
+  lazy val tru = parseFile(s"$prefix/true.ll")
+  lazy val fls = parseFile(s"$prefix/false.ll")
+  lazy val base32 = parseFile(s"$prefix/base32.ll")
+  lazy val base64 = parseFile(s"$prefix/base64.ll")
+  lazy val comm = parseFile(s"$prefix/comm.ll")
+  lazy val cut = parseFile(s"$prefix/cut.ll")
+  lazy val dirname = parseFile(s"$prefix/dirname.ll")
+  lazy val expand = parseFile(s"$prefix/expand.ll")
+  lazy val fold = parseFile(s"$prefix/fold.ll")
+  lazy val join = parseFile(s"$prefix/join.ll")
+  lazy val link = parseFile(s"$prefix/link.ll")
+  lazy val paste = parseFile(s"$prefix/paste.ll")
+  lazy val pathchk = parseFile(s"$prefix/pathchk.ll")
+}
+
 object TestComp {
   object ArrayExamples {
     val prefix = "benchmarks/test-comp/array-examples"
diff --git a/src/test/scala/gensym/TestCases.scala b/src/test/scala/gensym/TestCases.scala
index e213b93ac..c41a20fcc 100644
--- a/src/test/scala/gensym/TestCases.scala
+++ b/src/test/scala/gensym/TestCases.scala
@@ -160,60 +160,50 @@ object TestCases {
     TestPrg(kleefslib64Test, "kleelib64", "@main", noArg, noOpt, nPath(10)++status(0)),
   )
 
-  lazy val coreutils: List[TestPrg] = List(
-    TestPrg(echo_linked,    "echo_linked_posix",    "@main",  noMainFileOpt, "--argv=./echo.bc     --sym-stdout --sym-arg 2 --sym-arg 7", nPath(216136)++status(0)),
-    // [0.75008s/6.94065s/82.0174s] #blocks: 473/2224; #br: 160/96/1128; #paths: 216136; #threads: 1; #task-in-q: 0; #queries: 646097/53 (0)
-    // gcov 84.17%
-    TestPrg(cat_linked,     "cat_linked_posix",     "@main",  noMainFileOpt, "--argv=./cat.bc      --sym-stdout --sym-stdin 2 --sym-arg 2", nPath(28567)++status(0)),
-    // [17.5964s/122.277s/152.538s] #blocks: 1114/2484; #br: 371/297/1664; #paths: 28567; #threads: 1; #task-in-q: 0; #queries: 976797/71 (0)
-    // gcov 81.4%
-    TestPrg(base32_linked,  "base32_linked_posix",  "@main",  noMainFileOpt, "--argv=./base32      --sym-stdout  --sym-stdin 2 --sym-arg 2 -sym-files 2 2", nPath(10621)++status(0)),
-    // [11.0384s/81.2135s/95.0274s] #blocks: 1170/2718; #br: 417/284/1860; #paths: 10621; #threads: 1; #task-in-q: 0; #queries: 475353/38 (0)
-    // gcov 73.33%
-    TestPrg(base64_linked,  "base64_linked_posix",  "@main",  noMainFileOpt, "--argv=./base64.bc   --sym-stdout  --sym-stdin 2 --sym-arg 2 -sym-files 2 2", nPath(10624)++status(0)),
-    // [11.1519s/81.5593s/95.0264s] #blocks: 1164/2694; #br: 411/286/1889; #paths: 10624; #threads: 1; #task-in-q: 0; #queries: 475379/38 (0)
-    // gcov 73.33%
-    TestPrg(comm_linked,    "comm_linked_posix",    "@main",  noMainFileOpt, "--argv=./comm.bc     --sym-stdout  --sym-stdin 2 --sym-arg 2  --sym-arg 1 -sym-files 2 2", nPath(23846)++status(0)),
-    // [19.4591s/134.449s/164.537s] #blocks: 1230/2719; #br: 406/314/2077; #paths: 23846; #threads: 1; #task-in-q: 0; #queries: 993577/52 (0)
-    // gcov 72.41%
-    TestPrg(cut_linked,     "cut_linked_posix",     "@main",  noMainFileOpt, "--argv=./cut.bc      --sym-stdout  --sym-stdin 2 --sym-arg 2 --sym-arg  2 -sym-files 2 2", nPath(28481)++status(0)), // or --sym-args 0 2 2
-    // [31.0933s/98.3556s/134.029s] #blocks: 1056/2751; #br: 388/242/2124; #paths: 28481; #threads: 1; #task-in-q: 0; #queries: 238501/100 (0)
-    // gcov 67.44%
-    TestPrg(dirname_linked, "dirname_linked_posix", "@main",  noMainFileOpt, "--argv=./dirname.bc  --sym-stdout  --sym-stdin 2 --sym-arg 6 --sym-arg 10", nPath(287386)++status(0)),
-    // [1.14461s/18.4733s/115.025s] #blocks: 590/2295; #br: 219/93/2130; #paths: 287386; #threads: 1; #task-in-q: 0; #queries: 3720763/21 (0)
-    // gcov 100.00%
-    TestPrg(expand_linked,  "expand_linked_posix",  "@main",  noMainFileOpt, "--argv=./expand.bc   --sym-stdout  --sym-stdin 2 --sym-arg 2 -sym-files 2 2", nPath(10870)++status(0)),
-    // [21.482s/101.299s/116.022s] #blocks: 1167/2554; #br: 408/294/2145; #paths: 10870; #threads: 1; #task-in-q: 0; #queries: 478319/41 (0)
-    // gcov 71.05%
-    TestPrg(false_linked,   "false_linked_posix",   "@main",  noMainFileOpt, "--argv=./false.bc    --sym-stdout  --sym-arg 10", nPath(16)++status(0)),
-    // [0.012289s/0.032464s/1.00143s] #blocks: 391/2108; #br: 159/44/2276; #paths: 16; #threads: 1; #task-in-q: 0; #queries: 165/3 (0)
-    // gcov 100.00%
-    TestPrg(true_linked,    "true_linked_posix",    "@main",  noMainFileOpt, "--argv=./true.bc     --sym-stdout  --sym-arg 10", nPath(16)++status(0)),
-    // [0.012326s/0.032479s/1.0014s] #blocks: 391/2108; #br: 159/44/2276; #paths: 16; #threads: 1; #task-in-q: 0; #queries: 165/3 (0)
-    // gcov 100.00%
-    TestPrg(fold_linked,    "fold_linked_posix",    "@main",  noMainFileOpt, "--argv=./fold.bc     --sym-stdout  --sym-stdin 2 --sym-arg 2    -sym-files 2 2", nPath(11015)++status(0)),
-    // [11.2871s/95.8641s/110.53s] #blocks: 1212/2603; #br: 417/301/2279; #paths: 11015; #threads: 1; #task-in-q: 0; #queries: 478287/46 (0)
-    // gcov 74.36%
-    TestPrg(join_linked,    "join_linked_posix",    "@main",  noMainFileOpt, "--argv=./join.bc     --sym-stdout  --sym-stdin 2 --sym-arg 2 --sym-arg 1  -sym-files 2 2", nPath(25046)++status(0)),
-    // [32.7084s/230.442s/263.047s] #blocks: 1444/3172; #br: 461/369/2511; #paths: 25046; #threads: 1; #task-in-q: 0; #queries: 983311/87 (0)
-    // gcov 71.75%
-    TestPrg(link_linked,    "link_linked_posix",    "@main",  noMainFileOpt, "--argv=./link.bc     --sym-stdout  --sym-stdin 2 --sym-arg 2   --sym-arg 1  --sym-arg 1  -sym-files 2 2", nPath(11233)++status(0)),
-    // [9.39498s/116.469s/142.031s] #blocks: 891/2282; #br: 334/208/2511; #paths: 11233; #threads: 1; #task-in-q: 0; #queries: 1238401/91 (0)
-    // gcov 60.00%
-    TestPrg(paste_linked,   "paste_linked_posix",   "@main",  noMainFileOpt, "--argv=./paste.bc    --sym-stdout  --sym-stdin 2 --sym-arg 2 --sym-arg 1  -sym-files 2 2", nPath(22622)++status(0)),
-    // [19.9342s/142.499s/170.043s] #blocks: 1180/2510; #br: 393/306/2513; #paths: 22622; #threads: 1; #task-in-q: 0; #queries: 974269/46 (0)
-    // gcov 76.08%
-    TestPrg(pathchk_linked, "pathchk_linked_posix", "@main",  noMainFileOpt, "--argv=./pathchk.bc  --sym-stdout  --sym-stdin 2 --sym-arg 2", nPath(10614)++status(0)),
-    // [10.6848s/77.1473s/91.5263s] #blocks: 878/2418; #br: 314/226/2515; #paths: 10614; #threads: 1; #task-in-q: 0; #queries: 475423/30 (0)
-    // gcov 40.29%
-  )
-
   val all: List[TestPrg] = concrete ++ memModel ++ symbolicSimple ++ symbolicSmall ++ external ++ argv
+}
+
+object CoreutilsPOSIX {
+  // TODO: double check test configurations and spec
+  import ICSE23CoreutilsPOSIX._
+  lazy val coreutils: List[TestPrg] = List()
+  /*
+    TestPrg(echo,    "echo_linked_posix",    "@main",  noMainFileOpt, "--argv=./echo.bc --sym-stdout --sym-arg 2 --sym-arg 7", nPath(216136)++status(0)),
+    TestPrg(cat,     "cat_linked_posix",     "@main",  noMainFileOpt, "--argv=./cat.bc --sym-stdout --sym-stdin 2 --sym-arg 2", nPath(28567)++status(0)),
+    TestPrg(base32,  "base32_linked_posix",  "@main",  noMainFileOpt, "--argv=./base32 --sym-stdout  --sym-stdin 2 --sym-arg 2 -sym-files 2 2", nPath(10621)++status(0)),
+    TestPrg(base64,  "base64_linked_posix",  "@main",  noMainFileOpt, "--argv=./base64.bc --sym-stdout  --sym-stdin 2 --sym-arg 2 -sym-files 2 2", nPath(10624)++status(0)),
+    TestPrg(comm,    "comm_linked_posix",    "@main",  noMainFileOpt, "--argv=./comm.bc --sym-stdout  --sym-stdin 2 --sym-arg 2  --sym-arg 1 -sym-files 2 2", nPath(23846)++status(0)),
+    TestPrg(cut,     "cut_linked_posix",     "@main",  noMainFileOpt, "--argv=./cut.bc --sym-stdout  --sym-stdin 2 --sym-arg 2 --sym-arg  2 -sym-files 2 2", nPath(28481)++status(0)), // or --sym-args 0 2 2
+    TestPrg(dirname, "dirname_linked_posix", "@main",  noMainFileOpt, "--argv=./dirname.bc --sym-stdout  --sym-stdin 2 --sym-arg 6 --sym-arg 10", nPath(287386)++status(0)),
+    TestPrg(expand,  "expand_linked_posix",  "@main",  noMainFileOpt, "--argv=./expand.bc --sym-stdout  --sym-stdin 2 --sym-arg 2 -sym-files 2 2", nPath(10870)++status(0)),
+    TestPrg(fls,     "false_linked_posix",   "@main",  noMainFileOpt, "--argv=./false.bc --sym-stdout  --sym-arg 10", nPath(16)++status(0)),
+    TestPrg(tru,     "true_linked_posix",    "@main",  noMainFileOpt, "--argv=./true.bc --sym-stdout  --sym-arg 10", nPath(16)++status(0)),
+    TestPrg(fold,    "fold_linked_posix",    "@main",  noMainFileOpt, "--argv=./fold.bc --sym-stdout  --sym-stdin 2 --sym-arg 2    -sym-files 2 2", nPath(11015)++status(0)),
+    TestPrg(join,    "join_linked_posix",    "@main",  noMainFileOpt, "--argv=./join.bc --sym-stdout  --sym-stdin 2 --sym-arg 2 --sym-arg 1  -sym-files 2 2", nPath(25046)++status(0)),
+    TestPrg(link,    "link_linked_posix",    "@main",  noMainFileOpt, "--argv=./link.bc --sym-stdout  --sym-stdin 2 --sym-arg 2   --sym-arg 1  --sym-arg 1  -sym-files 2 2", nPath(11233)++status(0)),
+    TestPrg(paste,   "paste_linked_posix",   "@main",  noMainFileOpt, "--argv=./paste.bc --sym-stdout  --sym-stdin 2 --sym-arg 2 --sym-arg 1  -sym-files 2 2", nPath(22622)++status(0)),
+    TestPrg(pathchk, "pathchk_linked_posix", "@main",  noMainFileOpt, "--argv=./pathchk.bc --sym-stdout  --sym-stdin 2 --sym-arg 2", nPath(10614)++status(0)),
+  */
+}
 
-  // FIXME: out of range
-  // TestPrg(struct, "structTest", "@main", noArg, 1),
-  // FIXME: seg fault
-  // TestPrg(largeStackArray, "largeStackArrayTest", "@main", noArg, 1),
-  // TestPrg(makeSymbolicArray, "makeSymbolicArrayTest", "@main", noArg, 1),
-  // TestPrg(ptrtoint, "ptrToIntTest", "@main", noArg, 1)
+object CoreutilsUClibc {
+  import ICSE23CoreutilsPOSIX._
+  lazy val coreutils: List[TestPrg] = List()
+  /*
+    TestPrg(echo,    "echo_linked_uclibc",    "@main",  noMainFileOpt, "--argv=./echo.bc --sym-stdout --sym-arg 2 --sym-arg 7", nPath(216136)++status(0)),
+    TestPrg(cat,     "cat_linked_uclibc",     "@main",  noMainFileOpt, "--argv=./cat.bc --sym-stdout --sym-stdin 2 --sym-arg 2", nPath(28567)++status(0)),
+    TestPrg(base32,  "base32_linked_uclibc",  "@main",  noMainFileOpt, "--argv=./base32 --sym-stdout  --sym-stdin 2 --sym-arg 2 -sym-files 2 2", nPath(10621)++status(0)),
+    TestPrg(base64,  "base64_linked_uclibc",  "@main",  noMainFileOpt, "--argv=./base64.bc --sym-stdout  --sym-stdin 2 --sym-arg 2 -sym-files 2 2", nPath(10624)++status(0)),
+    TestPrg(comm,    "comm_linked_uclibc",    "@main",  noMainFileOpt, "--argv=./comm.bc --sym-stdout  --sym-stdin 2 --sym-arg 2  --sym-arg 1 -sym-files 2 2", nPath(23846)++status(0)),
+    TestPrg(cut,     "cut_linked_uclibc",     "@main",  noMainFileOpt, "--argv=./cut.bc --sym-stdout  --sym-stdin 2 --sym-arg 2 --sym-arg  2 -sym-files 2 2", nPath(28481)++status(0)), // or --sym-args 0 2 2
+    TestPrg(dirname, "dirname_linked_uclibc", "@main",  noMainFileOpt, "--argv=./dirname.bc --sym-stdout  --sym-stdin 2 --sym-arg 6 --sym-arg 10", nPath(287386)++status(0)),
+    TestPrg(expand,  "expand_linked_uclibc",  "@main",  noMainFileOpt, "--argv=./expand.bc --sym-stdout  --sym-stdin 2 --sym-arg 2 -sym-files 2 2", nPath(10870)++status(0)),
+    TestPrg(fls,     "false_linked_uclibc",   "@main",  noMainFileOpt, "--argv=./false.bc --sym-stdout  --sym-arg 10", nPath(16)++status(0)),
+    TestPrg(tru,     "true_linked_uclibc",    "@main",  noMainFileOpt, "--argv=./true.bc --sym-stdout  --sym-arg 10", nPath(16)++status(0)),
+    TestPrg(fold,    "fold_linked_uclibc",    "@main",  noMainFileOpt, "--argv=./fold.bc --sym-stdout  --sym-stdin 2 --sym-arg 2    -sym-files 2 2", nPath(11015)++status(0)),
+    TestPrg(join,    "join_linked_uclibc",    "@main",  noMainFileOpt, "--argv=./join.bc --sym-stdout  --sym-stdin 2 --sym-arg 2 --sym-arg 1  -sym-files 2 2", nPath(25046)++status(0)),
+    TestPrg(link,    "link_linked_uclibc",    "@main",  noMainFileOpt, "--argv=./link.bc --sym-stdout  --sym-stdin 2 --sym-arg 2   --sym-arg 1  --sym-arg 1  -sym-files 2 2", nPath(11233)++status(0)),
+    TestPrg(paste,   "paste_linked_uclibc",   "@main",  noMainFileOpt, "--argv=./paste.bc --sym-stdout  --sym-stdin 2 --sym-arg 2 --sym-arg 1  -sym-files 2 2", nPath(22622)++status(0)),
+    TestPrg(pathchk, "pathchk_linked_uclibc", "@main",  noMainFileOpt, "--argv=./pathchk.bc --sym-stdout  --sym-stdin 2 --sym-arg 2", nPath(10614)++status(0)),
+  */
 }
diff --git a/src/test/scala/gensym/TestGS.scala b/src/test/scala/gensym/TestGS.scala
index 3bebcd1a1..59e7624f8 100644
--- a/src/test/scala/gensym/TestGS.scala
+++ b/src/test/scala/gensym/TestGS.scala
@@ -29,6 +29,8 @@ import TestCases._
 abstract class TestGS extends FunSuite {
   import java.time.LocalDateTime
 
+  val cores: Option[Int] = None
+
   case class TestResult(time: LocalDateTime, commit: String, engine: String, testName: String,
     extSolverTime: Double, intSolverTime: Double, wholeTime: Double, blockCov: Double,
     partialBrCov: Double, fullBrCov: Double, pathNum: Int, brQueryNum: Int,
@@ -60,7 +62,10 @@ abstract class TestGS extends FunSuite {
                   else gs.insName + "_" + name
     test(name) {
       val code = gs.run(m, outname, f, config, libPath)
-      val mkRet = code.makeWithAllCores
+      val mkRet = cores match {
+        case None => code.makeWithHalfCores
+        case Some(n) => code.make(n)
+      }
       assert(mkRet == 0, "make failed")
       if (runCode) {
         val (output, ret) = code.runWithStatus(cliArg)
diff --git a/src/test/scala/icse23/CompileCoreutils.scala b/src/test/scala/icse23/CompileCoreutils.scala
new file mode 100644
index 000000000..596c4ba11
--- /dev/null
+++ b/src/test/scala/icse23/CompileCoreutils.scala
@@ -0,0 +1,55 @@
+package icse23
+
+import lms.core._
+import lms.core.Backend._
+import lms.core.virtualize
+import lms.macros.SourceContext
+import lms.core.stub.{While => _, _}
+
+import gensym._
+import gensym.lmsx._
+import gensym.llvm._
+import gensym.llvm.IR._
+import gensym.llvm.Benchmarks._
+import gensym.llvm.parser.Parser._
+import gensym.Config._
+import gensym.TestPrg._
+import gensym.TestCases._
+import gensym.Constants._
+import gensym.utils.Utils.time
+
+import sys.process._
+import org.scalatest.FunSuite
+
+/*
+
+class CompileCoreutilsPOSIX extends TestGS {
+  import gensym.llvm.parser.Parser._
+  Config.enableOpt
+  // Change None to Some(n) if you want to use n cores to compile c++ files with g++
+  override val cores: Option[Int] = None
+
+  val runtimeOptions = "--output-tests-cov-new --thread=1 --search=random-path --solver=z3 --output-ktest --cons-indep".split(" +").toList.toSeq
+  val cases = CoreutilsPOSIX.coreutils.map { t =>
+    t.copy(runOpt = runtimeOptions ++ t.runOpt, runCode = false)
+  }
+
+  testGS(new ImpCPSGS, cases)
+}
+
+class CompileCoreutilsUClibc extends TestGS {
+  import gensym.llvm.parser.Parser._
+  Config.enableOpt
+
+  // Change None to Some(n) if you want to use n cores to compile c++ files with g++
+  override val cores: Option[Int] = None
+
+  val runtimeOptions = "--output-tests-cov-new --thread=1 --search=random-path --solver=z3 --output-ktest --cons-indep".split(" +").toList.toSeq
+  val cases = CoreutilsUClibc.coreutils.map { t =>
+    t.copy(runOpt = runtimeOptions ++ t.runOpt, runCode = false)
+  }
+
+  testGS(new ImpCPSGS, cases)
+}
+
+*/
diff --git a/src/test/scala/icse23/KickTheTires.scala b/src/test/scala/icse23/KickTheTires.scala
new file mode 100644
index 000000000..bcc5d4ef0
--- /dev/null
+++ b/src/test/scala/icse23/KickTheTires.scala
@@ -0,0 +1,31 @@
+package icse23
+
+import lms.core._
+import lms.core.Backend._
+import lms.core.virtualize
+import lms.macros.SourceContext
+import lms.core.stub.{While => _, _}
+
+import gensym._
+import gensym.lmsx._
+import gensym.llvm._
+import gensym.llvm.IR._
+import gensym.llvm.Benchmarks._
+import gensym.llvm.parser.Parser._
+import gensym.Config._
+import gensym.TestPrg._
+import gensym.TestCases._
+import gensym.Constants._
+import gensym.utils.Utils.time
+
+import sys.process._
+import org.scalatest.FunSuite
+
+/*
+class KickTheTires extends TestGS {
+  import gensym.llvm.parser.Parser._
+  Config.enableOpt
+  val gs = new ImpCPSGS
+  testGS(gs, TestPrg(branch, "branch", "@f", symArg(2), noOpt, nPath(4)))
+}
+*/
diff --git a/third-party/lms-clean b/third-party/lms-clean
index 44af36bb0..b6f019aef 160000
--- a/third-party/lms-clean
+++ b/third-party/lms-clean
@@ -1 +1 @@
-Subproject commit 44af36bb07956c3edfd409e079a8251708c6060c
+Subproject commit b6f019aef1df5f1f12bcd0b43a9136d7f9ce7704