diff --git a/benchmarks/01-pure/10-nil_polymorphism.smt2 b/benchmarks/01-pure/10-nil_polymorphism.smt2
new file mode 100644
index 0000000..d56a265
--- /dev/null
+++ b/benchmarks/01-pure/10-nil_polymorphism.smt2
@@ -0,0 +1,13 @@
+(set-info :source Astral)
+(set-info :status sat)
+
+(declare-sort Loc 0)
+(declare-heap (Loc Loc))
+
+(declare-const x_ls  LS_t)
+(declare-const x_dls DLS_t)
+(declare-const x_nls NLS_t)
+
+(assert (= nil x_ls x_dls x_nls))
+
+(check-sat)
diff --git a/benchmarks/02-spatial_atoms/13-pointer_sequence_2.smt2 b/benchmarks/02-spatial_atoms/13-pointer_sequence_2.smt2
new file mode 100644
index 0000000..22af75a
--- /dev/null
+++ b/benchmarks/02-spatial_atoms/13-pointer_sequence_2.smt2
@@ -0,0 +1,17 @@
+(set-info :source Astral)
+(set-info :status sat)
+
+(declare-sort Loc 0)
+(declare-heap (Loc Loc))
+
+(declare-const x1 Loc)
+(declare-const x2 Loc)
+
+(assert
+  (sep
+    (pto x1 x2)
+    (pto x2 nil)
+  )
+)
+
+(check-sat)
diff --git a/benchmarks/03-lists/15-bound-example.smt2 b/benchmarks/03-lists/15-bound-example.smt2
new file mode 100644
index 0000000..04d65ce
--- /dev/null
+++ b/benchmarks/03-lists/15-bound-example.smt2
@@ -0,0 +1,28 @@
+(set-info :source Astral)
+(set-info :status unsat)
+
+(declare-sort Loc 0)
+(declare-heap (Loc Loc))
+
+(declare-const a Loc)
+(declare-const b Loc)
+(declare-const c Loc)
+(declare-const d Loc)
+
+(assert
+  (sep
+    (ls a b)
+    (pto b c)
+    (pto c d)
+    (ls d a)
+  )
+)
+
+(assert (not
+  (sep
+    (ls a c)
+    (ls c a)
+  )
+))
+
+(check-sat)
diff --git a/benchmarks/03-lists/16-same_root_sat.smt2 b/benchmarks/03-lists/16-same_root_sat.smt2
new file mode 100644
index 0000000..7472db2
--- /dev/null
+++ b/benchmarks/03-lists/16-same_root_sat.smt2
@@ -0,0 +1,18 @@
+(set-info :source Astral)
+(set-info :status sat)
+
+(declare-sort Loc 0)
+(declare-heap (Loc Loc))
+
+(declare-const x Loc)
+(declare-const y1 Loc)
+(declare-const y2 Loc)
+
+(assert
+  (sep
+    (ls x y1)
+    (ls x y2)
+  )
+)
+
+(check-sat)
diff --git a/benchmarks/03-lists/17-same_root_sat2.smt2 b/benchmarks/03-lists/17-same_root_sat2.smt2
new file mode 100644
index 0000000..826b27d
--- /dev/null
+++ b/benchmarks/03-lists/17-same_root_sat2.smt2
@@ -0,0 +1,19 @@
+(set-info :source Astral)
+(set-info :status sat)
+
+(declare-sort Loc 0)
+(declare-heap (Loc Loc))
+
+(declare-const x Loc)
+(declare-const y1 Loc)
+(declare-const y2 Loc)
+
+(assert
+  (sep
+    (distinct y1 y2)
+    (ls x y1)
+    (ls x y2)
+  )
+)
+
+(check-sat)
diff --git a/benchmarks/03-lists/18-same_root_unsat.smt2 b/benchmarks/03-lists/18-same_root_unsat.smt2
new file mode 100644
index 0000000..8b04548
--- /dev/null
+++ b/benchmarks/03-lists/18-same_root_unsat.smt2
@@ -0,0 +1,19 @@
+(set-info :source Astral)
+(set-info :status unsat)
+
+(declare-sort Loc 0)
+(declare-heap (Loc Loc))
+
+(declare-const x Loc)
+(declare-const y1 Loc)
+(declare-const y2 Loc)
+
+(assert
+  (sep
+    (distinct x y1 y2)
+    (ls x y1)
+    (ls x y2)
+  )
+)
+
+(check-sat)
diff --git a/benchmarks/05-wands/config.yaml b/benchmarks/05-wands/config.yaml
new file mode 100644
index 0000000..f12799f
--- /dev/null
+++ b/benchmarks/05-wands/config.yaml
@@ -0,0 +1 @@
+ignore: True
diff --git a/benchmarks/06-symbolic_heaps_sat/config.yaml b/benchmarks/06-symbolic_heaps_sat/config.yaml
new file mode 100644
index 0000000..19ae0dc
--- /dev/null
+++ b/benchmarks/06-symbolic_heaps_sat/config.yaml
@@ -0,0 +1 @@
+verify-model: true
diff --git a/benchmarks/09-negative/config.yaml b/benchmarks/09-negative/config.yaml
new file mode 100644
index 0000000..9666bb8
--- /dev/null
+++ b/benchmarks/09-negative/config.yaml
@@ -0,0 +1,4 @@
+separation: "weak"
+
+#restrict_encodings: ["sets"]
+#restrict_qelims: ["none"]
diff --git a/benchmarks/15-strong-separation/01-list_length2_unsat.smt2 b/benchmarks/15-SSL/01-list_length_geq_2_unsat.smt2
similarity index 100%
rename from benchmarks/15-strong-separation/01-list_length2_unsat.smt2
rename to benchmarks/15-SSL/01-list_length_geq_2_unsat.smt2
diff --git a/benchmarks/15-strong-separation/02-list_length2_sat.smt2 b/benchmarks/15-SSL/02-list_length_geq_2_sat.smt2
similarity index 100%
rename from benchmarks/15-strong-separation/02-list_length2_sat.smt2
rename to benchmarks/15-SSL/02-list_length_geq_2_sat.smt2
diff --git a/benchmarks/15-SSL/03-list_length_eq_2_unsat.smt2 b/benchmarks/15-SSL/03-list_length_eq_2_unsat.smt2
new file mode 100644
index 0000000..b4990cb
--- /dev/null
+++ b/benchmarks/15-SSL/03-list_length_eq_2_unsat.smt2
@@ -0,0 +1,27 @@
+(set-info :source Astral)
+(set-info :status unsat)
+
+(declare-sort Loc 0)
+(declare-heap (Loc Loc))
+
+(declare-const x Loc)
+(declare-const y Loc)
+
+(assert (ls x y))
+
+(assert
+  (sep
+    (not sep.emp)
+    (not sep.emp)
+  )
+)
+
+(assert (not
+  (sep
+    (not sep.emp)
+    (not sep.emp)
+    (not sep.emp)
+  )
+))
+
+(check-sat)
diff --git a/benchmarks/15-SSL/04-list_length_eq_2_sat.smt2 b/benchmarks/15-SSL/04-list_length_eq_2_sat.smt2
new file mode 100644
index 0000000..9ff8af4
--- /dev/null
+++ b/benchmarks/15-SSL/04-list_length_eq_2_sat.smt2
@@ -0,0 +1,28 @@
+(set-info :source Astral)
+(set-info :status sat)
+
+(declare-sort Loc 0)
+(declare-heap (Loc Loc))
+
+(declare-const x Loc)
+(declare-const y Loc)
+(declare-const z Loc)
+
+(assert (ls x y))
+
+(assert
+  (sep
+    (not sep.emp)
+    (not sep.emp)
+  )
+)
+
+(assert (not
+  (sep
+    (not sep.emp)
+    (not sep.emp)
+    (not sep.emp)
+  )
+))
+
+(check-sat)
diff --git a/benchmarks/15-strong-separation/03-list_length3_unsat.smt2 b/benchmarks/15-SSL/05-list_length_geq_3_unsat_v1.smt2
similarity index 100%
rename from benchmarks/15-strong-separation/03-list_length3_unsat.smt2
rename to benchmarks/15-SSL/05-list_length_geq_3_unsat_v1.smt2
diff --git a/benchmarks/15-strong-separation/04-list_length3_unsat2.smt2 b/benchmarks/15-SSL/06-list_length_geq_3_unsat_v2.smt2
similarity index 100%
rename from benchmarks/15-strong-separation/04-list_length3_unsat2.smt2
rename to benchmarks/15-SSL/06-list_length_geq_3_unsat_v2.smt2
diff --git a/benchmarks/15-strong-separation/05-list_length3_sat.smt2 b/benchmarks/15-SSL/07-list_length3_sat.smt2
similarity index 100%
rename from benchmarks/15-strong-separation/05-list_length3_sat.smt2
rename to benchmarks/15-SSL/07-list_length3_sat.smt2
diff --git a/benchmarks/15-SSL/config.yaml b/benchmarks/15-SSL/config.yaml
new file mode 100644
index 0000000..489591b
--- /dev/null
+++ b/benchmarks/15-SSL/config.yaml
@@ -0,0 +1 @@
+separation: "strong"
diff --git a/scripts/run_test_case.py b/scripts/run_test_case.py
new file mode 100644
index 0000000..9034ea7
--- /dev/null
+++ b/scripts/run_test_case.py
@@ -0,0 +1,130 @@
+# Runner of a single test case
+#
+# Author: Tomas Dacik (idacik@fit.vut.cz), 2024
+
+import os
+import yaml
+
+from dataclasses import dataclass
+from enum import Enum
+from subprocess import run, PIPE, TimeoutExpired
+
+from utils import *
+
+ASTRAL = "_build/default/main.exe"
+TMP = "/tmp/astral"
+
+
+@dataclass
+class Config:
+    ignore: bool = False
+    verify_model: bool = False  # TODO: implement
+
+    timeout: int = 10
+    backend: str = "z3"
+    encoding: str = "bitvectors"
+    qf_encoding: str = "direct"
+    separation: str = "weak"
+
+    @classmethod
+    def from_file(cls, path):
+        with open(path, "r") as f:
+            json = yaml.safe_load(f)
+
+        kwargs = {
+            key.replace("-", "_"): value for key, value in json.items()
+        }  # if key in vars(Config)}
+        return Config(**kwargs)
+
+    def to_command(self, path):
+        name = os.path.basename(path)
+        # fmt: off
+        return [
+            ASTRAL,
+            "--backend", self.backend,
+            "--encoding", self.encoding,
+            "--qf-encoding", self.qf_encoding,
+            "--separation", self.separation,
+            "--json-output", TMP + name + ".json",
+            path
+        ]
+        # fmt: on
+
+
+class Status(Enum):
+    CORRECT = 0
+    INCORRECT = 1
+    UNKNOWN = 2
+    TIMEOUT = 3
+    ERROR = 4
+
+
+@dataclass
+class Result:
+    name: str
+    status: Status
+    return_code: int = 0
+
+    @classmethod
+    def of_run(cls, name, process):
+        stdout = process.stdout.decode().strip()
+        stderr = process.stderr.decode().strip()
+
+        if process.returncode == 0 and stdout.startswith("unknown"):
+            status = Status.UNKNOWN
+        elif process.returncode == 0:
+            status = Status.CORRECT
+        elif process.returncode == 1:
+            status = Status.INCORRECT
+        else:
+            status = Status.ERROR
+
+        return Result(name, status, process.returncode)
+
+    @classmethod
+    def timeout(cls, name, to):
+        return Result(name, Status.TIMEOUT)
+
+    @property
+    def is_correct(self):
+        return self.status == Status.CORRECT
+
+    @property
+    def is_unknown(self):
+        return self.status in [Status.UNKNOWN, Status.TIMEOUT]
+
+    def is_error(self):
+        return not self.is_correct and not self.is_unknown
+
+    def print(self):
+        if self.status == Status.CORRECT:
+            print_ok(f"[OK] {self.name}")
+        elif self.status == Status.UNKNOWN:
+            print_unknown(f"[UNKNOWN] {self.name}")
+        elif self.status == Status.TIMEOUT:
+            print_unknown(f"[TIMEOUT]: {self.name}")
+        elif self.status == Status.INCORRECT:
+            print_err(f"[INCORRECT]: {self.name}")
+        else:
+            print_err(f"[ERR {self.return_code}]: {self.name}")
+
+
+class TestRunner:
+    def __init__(self, path, config=Config()):
+        self.path = path
+        self.name = os.path.basename(path)
+        self.config = config
+        self.result = None
+
+    def run(self):
+        command = self.config.to_command(self.path)
+        try:
+            process = run(
+                command, timeout=self.config.timeout, stdout=PIPE, stderr=PIPE
+            )
+            result = Result.of_run(self.name, process)
+        except TimeoutExpired as to:
+            result = Result.timeout(self.name, to)
+
+        result.print()
+        return result
diff --git a/scripts/run_tests.py b/scripts/run_tests.py
index e61bf66..489b530 100644
--- a/scripts/run_tests.py
+++ b/scripts/run_tests.py
@@ -1,115 +1,101 @@
-# Runner of regression tests
+# Runner of all test cases
 #
-# Author: Tomas Dacik (idacik@fit.vut.cz), 2022
+# Author: Tomas Dacik (idacik@fit.vut.cz), 2024
 
 import os
 import shutil
 
-from subprocess import run, PIPE, TimeoutExpired
-
 from utils import *
-from property_checker import check
-
-astral_bin = "_build/default/main.exe"
-
+from run_test_case import Config, TestRunner, Status
 
-def print_bench_name(root, dirs):
-    print(os.path.basename(root))
+ASTRAL = "_build/default/main.exe"
+TMP = "/tmp/astral"
 
 
 class Runner:
-    def __init__(
-        self, backend="z3", encoding="bitvectors", qf_encoding="direct", timeout=10
-    ):
-        self.backend = backend
-        self.encoding = encoding
-        self.qf_encoding = qf_encoding
+    def __init__(self, verbose=True):
+        self.default_config = Config()
+        self.verbose = verbose
 
-        self.timeout = timeout
+        self.results = {}
 
-        self.correct = 0
-        self.incorrect = 0
-        self.unknown = 0
-
-        self.errors = 0
-        self.timeouts = 0
+    def print_bench_name(self, root, ignore=False):
+        if self.verbose:
+            if ignore:
+                print(os.path.basename(root), "[Skipped]")
+            else:
+                print(os.path.basename(root))
 
     def smoke_test(self):
         """Verify whether Astral is correctly installed."""
         try:
-            process = run([astral_bin, "--help"], stdout=PIPE, stderr=PIPE)
+            pass
+            # process = run([ASTRAL, "--help"], stdout=PIPE, stderr=PIPE)
         except FileNotFoundError:
             print_err("Astral is not correctly installed")
             exit(1)
 
-    def run(self, path, name):
-        # fmt: off
-        command = [
-            astral_bin,
-            "--backend", self.backend,
-            "--encoding", self.encoding,
-            "--qf-encoding", self.qf_encoding,
-            "--separation", "weak",
-            "--json-output", "/tmp/astral/" + name + ".json",
-            os.path.join(path, name),
-        ]
-        # fmt: on
-        try:
-            process = run(command, timeout=self.timeout, stdout=PIPE, stderr=PIPE)
-            stdout = process.stdout.decode().strip()
-            stderr = process.stderr.decode().strip()
+    def init(self):
+        shutil.rmtree(TMP, ignore_errors=True)
+        os.mkdir(TMP)
 
-            if process.returncode == 0:
-                print_ok(f"[OK] {name}: {stdout}")
-                self.correct += 1
+    def run_test_case(self, path, config):
+        runner = TestRunner(path, config)
+        return runner.run()
 
-                # Check additional properties
-                #check(os.path.join(path, name), "/tmp/astral/" + name + ".json")
+    def run_test_suite(self, directory, files):
+        # Load configuration, if specified
+        try:
+            config = Config.from_file(os.path.join(directory, "config.yaml"))
+        except FileNotFoundError:
+            config = self.default_config
 
-            elif process.returncode == 2:
-                print_err(f"[INCORRECT]: {name}: {stdout}")
-                print(stdout)
-                print(stderr)
-                self.incorrect += 1
+        self.print_bench_name(directory, ignore=config.ignore)
+        if config.ignore:
+            return
 
-            else:
-                print_err(f"[ERR {process.returncode}]: {name}: {stdout}")
-                self.errors += 1
+        print(config)
+        for f in sorted(files):
+            if f.endswith(".smt2"):
+                path = os.path.join(directory, f)
+                result = self.run_test_case(path, config)
+                self.results[result.name] = result
 
-        except TimeoutExpired as to:
-            print_unknown(f"[TO]: {name}")
-            self.timeouts += 1
+    def run_all(self):
+        for root, dirs, files in sorted(os.walk("benchmarks/")):
+            if "astral_debug" in root or "TODO" in root or root == "benchmarks/":
+                # Ignore debug and TODOs directories
+                continue
 
-    def print_result(self):
-        if runner.incorrect > 0:
-            print_err(" - incorrect: ", runner.incorrect)
-        if runner.errors > 0:
-            print_err(" - errors: ", runner.incorrect)
-        if runner.timeouts > 0:
-            print_err(" - timeouts: ", runner.timeouts)
+            self.run_test_suite(root, files)
 
-    def clean(self):
-        shutil.rmtree("/tmp/astral", ignore_errors=True)
+    def report(self):
+        correct = len([x for x in self.results.values() if x.status == Status.CORRECT])
+        incorrect = len(
+            [x for x in self.results.values() if x.status == Status.INCORRECT]
+        )
+        timeout = len([x for x in self.results.values() if x.status == Status.TIMEOUT])
+        error = len([x for x in self.results.values() if x.status == Status.ERROR])
+        unknown = len([x for x in self.results.values() if x.status == Status.UNKNOWN])
 
-    def init(self):
-        self.clean()
-        os.mkdir("/tmp/astral")
+        total = len(self.results)
 
-    def run_one(self):
-        self.init()
-        for root, dirs, files in sorted(os.walk("benchmarks/")):
-            if os.path.basename(root) in ["astral_debug"]:
-                # Ignore debug directories
-                continue
+        print(f"\nTotal tests: {total}")
 
-            print_bench_name(root, dirs)
-            for f in sorted(files):
-                if f.endswith(".smt2"):
-                    self.run(root, f)
-        self.clean()
+        if incorrect > 0:
+            print_err(f" - incorrect: {incorrect}")
+        if error > 0:
+            print_err(f" - errors: {error}")
+
+        if incorrect + error > 0:
+            return 1
+        return 0
 
 
 if __name__ == "__main__":
     runner = Runner()
+    runner.init()
     runner.smoke_test()
-    runner.run_one()
+    runner.run_all()
+
+    exit(runner.report())