diff --git a/benchmark_comparison.py b/benchmark_comparison.py
index 7082e5a..df78a20 100755
--- a/benchmark_comparison.py
+++ b/benchmark_comparison.py
@@ -5,29 +5,39 @@
 import sympy as sp
 import os
 from glob import glob
-
+import re
 
 # All files in the pgfexamples folder
+# https://stackoverflow.com/a/18394205
 all_files: list[str] = [y for x in os.walk("pgfexamples") for y in glob(os.path.join(x[0], '*.pgcl'))] + [
     "example.pgcl"]
 
 # Timeouts / Exception runs
 # If files are not present, an empty list is returned
-timeouts: list[str] = list(map(str.strip, open("timeouts.txt", "r").readlines())) \
-    if os.path.isfile("timeouts.txt") else [] + \
-    list(map(str.strip, open("exceptions.txt", "r").readlines())) if os.path.isfile("exceptions.txt") else []
+skip_files: list[str] = (list(map(str.strip, open("timeouts.txt", "r").readlines())) \
+    if os.path.isfile("timeouts.txt") else []) + \
+                                           (list(map(str.strip,
+                                                    open("exceptions.txt", "r").readlines())) if os.path.isfile(
+    "exceptions.txt") else [])
 
 # All available engines
 # (will be executed in this order)
-engines = [
+engines: list[str] = [
     "ginac", "symengine", "sympy"
 ]
 
+# Default CLI args for files that do not contain any additional information
+default_instruction: list[str] = ["main"]
+
+# https://stackoverflow.com/a/14693789
+ansi_escape = re.compile(r'\x1B(?:[@-Z\\-_]|\[[0-?]*[ -/]*[@-~])')
+
 
 class Run:
     """
     Represents a single run of one engine on one file.
     """
+
     def __init__(self, time, output, file):
         """
         Initializes the Run object.
@@ -60,6 +70,7 @@ class Configuration:
     """
     Represents the configuration given by the user
     """
+
     def __init__(self, args):
         """
         Initializes the Configuration object.
@@ -85,6 +96,9 @@ def __init__(self, args):
         elif "pgcl" in input_files:
             # A single file should be tested
             self.files = [args.input]
+        elif os.path.isdir(input_files):
+            # A folder is given, only test files in the folder
+            self.files = [y for x in os.walk(args.input) for y in glob(os.path.join(x[0], '*.pgcl'))]
         else:
             # A file containing files that should be tested
             self.files = list(map(str.strip, open(input_files, "r").readlines()))
@@ -113,7 +127,8 @@ def create_parser() -> argparse.ArgumentParser:
         "input",
         metavar="INPUT",
         help="File to be analyzed. If set to \"all\", all files in the pgfexamples folder will be analyzed. " +
-             "If file does not have a .pgcl extension, it is interpreted to be a file containing files to be tested.",
+             "If a folder is provided, all files with '.pgcl' extensions in the folder or its subfolders are tested. " +
+             "If  file does not have a .pgcl extension, it is interpreted to be a file containing files to be tested.",
         type=str
     )
 
@@ -123,7 +138,7 @@ def create_parser() -> argparse.ArgumentParser:
         "--engine",
         metavar="ENGINE",
         help="The engine that should be tested primarily. Separate multiple engines by ','. " +
-             "If unset, all engines are tested. Note: Engines will be executed in the order given. "+
+             "If unset, all engines are tested. Note: Engines will be executed in the order given. " +
              f"Supported engines: {', '.join(engines)}."
     )
 
@@ -210,51 +225,68 @@ def benchmark(config: Configuration):
 
     # If output is wanted, set up the corresponding file
     if config.output_file is not None:
-        setup_outfile(config.output_file)
+        setup_outfile(config.output_file, config.engine)
 
     counter = 0
     # For each file, test all engines
     for file in config.files:
         counter += 1
         print(f"Now testing: {file} ({counter}/{len(config.files)})")
-
         # Check if the current file is in timeouts
-        if file in timeouts and config.skip_timeouts:
-            print(f"File is in timeouts, skipping...")
+        if file in skip_files and config.skip_timeouts:
+            print(f"File is in skipped files, skipping...")
             continue
         engine_counter = 0
+
+        instructions = obtain_instructions(file)
+        # Check if file is to be skipped
+        if not instructions:
+            print("File marked to be skipped...")
+            continue
+
+        inputs = obtain_inputs(instructions)
+
+        skipped = False
         # For each engine, run the program
         for engine in config.engine:
+            if skipped:
+                continue
+
             engine_counter += 1
             print(f"Running {engine} ({engine_counter}/{len(config.engine)})")
 
             # Check if current file is in timeouts
             # Files can be added dynamically, hence the second check
-            if file in timeouts and config.skip_timeouts:
-                print(f"File is in timeouts, skipping...")
+            if file in skip_files and config.skip_timeouts:
+                print(f"File is in skipped files, skipping...")
+                skipped = True
                 continue
 
             output = ""
             # Execute the program
+            cmd = ["python", "prodigy/cli.py", "--engine", engine, *instructions]
+            print(bytes.decode(inputs))
             try:
-                cmd = ["python", "prodigy/cli.py", "--engine", engine, "main", file]
-                output = subprocess.check_output(cmd, timeout=config.timeout).decode()
-                print(output)
+                output = subprocess.check_output(cmd, timeout=config.timeout, input=inputs).decode()
             except TimeoutExpired as e:
                 # Command timed out
+                print("Command timed out, writing in timeouts.txt...")
                 with open("timeouts.txt", "a") as f:
                     # Write the file in "timeouts.txt" and add to the list
                     f.write(file + "\n")
-                    timeouts.append(file)
+                    skip_files.append(file)
+                    skipped = True
                     if config.fail_on_error:
                         raise e
                     continue
             except subprocess.CalledProcessError as e:
+                print("Command threw an exception, writing in exceptions.txt...")
                 # Error occurred while running the program (e.g. runtime error)
                 with open("exceptions.txt", "a") as f:
                     # Write the file in "timeouts.txt" and add to the list
                     f.write(file + "\n")
-                    timeouts.append(file)
+                    skip_files.append(file)
+                    skipped = True
                     if config.fail_on_error:
                         raise e
                     continue
@@ -263,121 +295,242 @@ def benchmark(config: Configuration):
                 raise RuntimeError("No output was captured.")
 
             # Parse output
+            print(output)
             output = output.splitlines()
+            run = capture_output(output, instructions, file)
+            print(run)
 
-            # Sometimes other stuff is logged, which is captured
-            # but not interesting for the analysis.
-            # The interesting part begins with "Result: [...]"
-            while "Result" not in output[0]:
-                output = output[1:]
-
-            # Add time to the dictionary
-            times[engine].append(
-                Run(
-                    time=float(output[-1].split()[-2]),
-                    output=tuple(
-                        str(
-                            output[0]
-                            .split("\x1b")[2]
-                            .split("[92m")[1]
-                        ).removeprefix("(")
-                        .removesuffix(")")
-                        .split(",")
-                    ),  # Very hacky lol
-                    file=file
-                )
-            )
+            # Add the result to the dictionary
+            times[engine].append(run)
+        fail = False
 
         # Compare results if at least two engines are selected and file wasn't skipped once (if skip_timeouts is set)
-        if len(config.engine) > 1 and (not config.skip_timeouts or file not in timeouts):
-            try:
-                results: dict[str, list[sp.Expr]] = {}
-                for engine in config.engine:
-                    # Results for "engine" look like this:
-                    #   expr, error_prob
-                    results[engine] = [sp.S(times[engine][-1].output[i]) for i in range(2)]
-            except Exception as e:
-                # Something went wrong while parsing
-                print(str(e))
-                if config.fail_on_error:
-                    raise e
-                continue
-
-            fail = False
-            # Compare all results
-            for engine in config.engine:
-                if fail:
-                    break
-                # Engines the current engine is compared against
-                # Technically, we only need one direction of equality
-                # but this is more convenient
-                other_engines = set(results.keys()) - {engine}
-                for other_engine in other_engines:
-                    if fail:
-                        break
-                    # Compare expr and error_prob
-                    for i in range(2):
-                        if fail:
-                            break
-                        try:
-                            assert results[engine][i].equals(results[other_engine][i]), \
-                                f"""
-                                Engine {engine} disagrees with engine {other_engine} on file {file}.
-                                """ + "\n".join(f"{e}: {results[e][i]}" for e in engines)
-                        except AssertionError as e:
-                            with open("exceptions.txt", "a") as f:
-                                # Write file to exception file
-                                # We do not need to add file to timeouts,
-                                # as the file was already checked
-                                f.write(file + "\n")
-                            print(str(e))
-                            if config.fail_on_error:
-                                raise e
-                            fail = True
-                            break
-
-            # Results are equal, add run to output file (if set)
-            if config.output_file is not None and not fail:
-                with open(config.output_file, "a") as f:
-                    f.write(file)
-                    for engine in config.engine:
-                        f.write(f",{times[engine][-1].time}")
-                    f.write("\n")
-
+        if len(config.engine) > 1 and not skipped:
+            fail = compare_output({engine: times[engine][-1] for engine in config.engine}, instructions, file,
+                                  config.fail_on_error)
             if not fail:
                 print("Results are equal, continuing...")
 
+        # Write results if output file is set (and results are equal or just one engine is tested)
+        if config.output_file is not None and not fail and not skipped:
+            with open(config.output_file, "a") as f:
+                f.write(file)
+                for engine in config.engine:
+                    f.write(f",{times[engine][-1].time}")
+                f.write("\n")
     # If generate markdown is set, create the Markdown table
     if config.generate_markdown:
         print("Generating markdown table...")
         generate_markdown_table(config.output_file, config.engine)
 
 
-def setup_outfile(out_file: str):
+def setup_outfile(out_file: str, engine_list: list[str]) -> None:
+    """
+    Creates the output csv file and writes the header. If a file of the same name already exists, rename it to <name>_{i},
+    where i is the lowest number such that no file with the name <name>_i exists.
+    :param out_file: The file to be created.
+    :param engine_list: The list of engines which are tested.
+    """
     # If file exists, rename it to filename_{i}.extension
     if os.path.isfile(out_file):
         i = 1
-        new_name = out_file.split(".")[0] + f"_{i}." + out_file.split(".")[1]
+        new_name_template = lambda el: out_file.split(".")[0] + f"_{el}." + out_file.split(".")[1]
+        new_name = new_name_template(i)
         while os.path.isfile(new_name):
             i += 1
-            new_name = out_file.split(".")[0] + f"_{i}." + out_file.split(".")[1]
+            new_name = new_name_template(i)
         os.rename(out_file, new_name)
 
     # Write header
     with open(out_file, "a") as f:
         f.write("file")
-        for engine in engines:
+        for engine in engine_list:
             f.write(f",{engine}")
         f.write("\n")
 
 
-def generate_markdown_table(csv_file: str, engine_list: list[str]):
+def obtain_instructions(file_path: str) -> list[str]:
+    """
+    Reads the first line of given file and checks whether it is instructions for the command
     """
-    Parses a given csv file to a Markdown table while highlighting the fastest result
+
+    with open(file_path, "r") as f:
+        first_line = f.readlines()[0]
+
+    if first_line.startswith("#"):
+        # First line is an instruction
+        parts = list(map(str.strip, first_line.split()[1:]))
+        # If "skip" is set, the file should be ignored
+        if parts == ["skip"]:
+            return []
+        return parts
+    else:
+        # No instruction is given -> return the default instruction
+        print(f"No instruction found for {file_path}, executing default instruction...")
+        return default_instruction + [file_path]
+
+def obtain_inputs(instructions: list[str]) -> bytes:
+    if len(instructions) == 2:
+        # No input is necessary
+        return b""
+    method = instructions[0]
+    other_file = instructions[2]
+    input_cmd = b""
+    if method == "check_equality" and ("loopy" in other_file or "template_parameter_synthesis"):
+        if other_file.endswith("1.pgcl"):
+            # We have multiple invariants
+            input_cmd = str.encode("".join("1\n" + inv_file + "\n" for inv_file in
+                                           list(sorted(glob(other_file.replace("1.pgcl", "*"))))))
+        else:
+            # Select invariant file for loopy programs
+            input_cmd = b"1\n" + str.encode(other_file + "\n")
+    return input_cmd
+
+def capture_output(output: list[str], cmd: list[str], file: str) -> Run:
+    # Remove ANSI
+    output = [ansi_escape.sub("", o) for o in output]
+    if "main" in cmd:
+        # Sometimes other stuff is logged, which is captured
+        # but not interesting for the analysis.
+        # The interesting part begins with "Result: [...]"
+        while "Result" not in output[0]:
+            output = output[1:]
+        return Run(
+            time=float(output[-1].split()[-2]),
+            output=tuple(
+                str(output[0].split("\t")[1])
+                .removeprefix("(")
+                .removesuffix(")")
+                .split(",")
+            ),
+            file=file
+        )
+    elif "check_equality" in cmd:
+        # TODO check parameter for parameter synthesis?
+        while "equivalent" not in output[0]:
+            output = output[1:]
+        return Run(
+            time=float(output[-1].split()[-2]),
+            output=(output[0].startswith("Program is equivalent to invariant")),
+            file=file
+        )
+    elif "invariant_synthesis" in cmd:
+        while "Invariant: " not in output[0]:
+            output = output[1:]
+        return Run(
+            time=float(output[-1].split()[-2]),
+            output=output[0].split("Invariant: ")[1],
+            file=file
+        )
+    else:
+        # todo other methods
+        pass
+
+
+def compare_output(outputs: dict[str, Run], cmd: list[str], file: str, fail_on_error: bool) -> bool:
+    fail = False
+    if "main" in cmd:
+        parsed_results: dict[str, tuple[sp.Expr, sp.Expr]] = {}
+        for engine in outputs.keys():
+            try:
+                parsed_results[engine] = (sp.S(outputs[engine].output[0]), sp.S(outputs[engine].output[0]))
+            except Exception as e:
+                print(str(e))
+                if fail_on_error:
+                    raise e
+
+        for engine in outputs.keys():
+            other_engines = set(outputs.keys()) - {engine}
+            for other_engine in other_engines:
+                if fail:
+                    break
+                for i in range(2):
+                    if fail:
+                        break
+                    try:
+                        assert parsed_results[engine][i].equals(parsed_results[other_engine][i]), \
+                            f"""
+                                Engine {engine} disagrees with {other_engine} on file {file}.
+                            """ + "\n".join(f"{e}: {parsed_results[e][i]}" for e in engines)
+                    except AssertionError as e:
+                        fail = True
+                        with open("exceptions.txt", "a") as f:
+                            # Write file to exception file
+                            # We do not need to add file to timeouts,
+                            # as the file was already checked
+                            f.write(file + "\n")
+                        print(str(e))
+                        if fail_on_error:
+                            raise e
+                        break
+    elif "equivalence" in cmd:
+        for engine in outputs.keys():
+            other_engines = set(outputs.keys()) - {engine}
+            for other_engine in other_engines:
+                if fail:
+                    break
+                try:
+                    assert outputs[engine].output == outputs[other_engine].output, \
+                        f"""
+                            Engine {engine} disagrees with {other_engine} on file {file}.
+                        """ + "\n".join(f"{e}: {outputs[e].output}" for e in engines)
+                except AssertionError as e:
+                    fail = True
+                    with open("exceptions.txt", "a") as f:
+                        # Write file to exception file
+                        # We do not need to add file to timeouts,
+                        # as the file was already checked
+                        f.write(file + "\n")
+                    print(str(e))
+                    if fail_on_error:
+                        raise e
+                    break
+    elif "invariant_synthesis" in cmd:
+        parsed_results: dict[str, sp.Expr] = {}
+        for engine in outputs.keys():
+            try:
+                parsed_results[engine] = sp.S(outputs[engine].output)
+            except Exception as e:
+                print(str(e))
+                if fail_on_error:
+                    raise e
+        for engine in outputs.keys():
+            other_engines = set(outputs.keys()) - {engine}
+            for other_engine in other_engines:
+                if fail:
+                    break
+                try:
+                    assert parsed_results[engine].equals(parsed_results[other_engine]), \
+                        f"""
+                            Engine {engine} disagrees with {other_engine} on file {file}.
+                        """ + "\n".join(f"{e}: {parsed_results[e]}" for e in engines)
+                except AssertionError as e:
+                    fail = True
+                    with open("exceptions.txt", "a") as f:
+                        # Write file to exception file
+                        # We do not need to add file to timeouts,
+                        # as the file was already checked
+                        f.write(file + "\n")
+                    print(str(e))
+                    if fail_on_error:
+                        raise e
+                    break
+    else:
+        # TODO other methods
+        pass
+    return fail
+
+
+def generate_markdown_table(csv_file: str, engine_list: list[str]) -> None:
+    """
+    Parses a given csv file to a Markdown table while highlighting the fastest result.
 
     :param csv_file: The csv file to be parsed.
     :param engine_list: A list of engines to be compared.
     """
+
+    # TODO should number of skipped runs be logged?
+
     out_file = csv_file.split(".")[0] + "_format.md"
 
     # Read the output file
@@ -416,8 +569,11 @@ def generate_markdown_table(csv_file: str, engine_list: list[str]):
                 # Write the run
                 f.write("|" + "|".join(line) + "|\n")
         # Write the average and summary
-        f.write("|Average|" + "|".join([f"{sum(results[i]) / len(results[i])}" for i in range(len(engine_list))]) + "|\n")
-        f.write("Times fastest run|" + "|".join(map(str, no_fastest)) + "|\n")
+        f.write(
+            "|Average|" + "|".join([f"{sum(results[i]) / len(results[i])}" for i in range(len(engine_list))]) + "|\n")
+        # Only add the time comparison if at least 2 engines are selected
+        if len(engine_list) > 1:
+            f.write("Times fastest run|" + "|".join(map(str, no_fastest)) + "|\n")
 
 
 if __name__ == '__main__':
diff --git a/pgfexamples/README.md b/pgfexamples/README.md
index 89d3aa9..92d563d 100644
--- a/pgfexamples/README.md
+++ b/pgfexamples/README.md
@@ -7,17 +7,47 @@ pgfexamples/
 ├── comparison                      # Comparisons with other tools / paradigms
 │   ├── ADDcomparison               # Comparisons with Algebraic Decision Diagrams
 │   └── psicomparison               # Comparisons with Psi
-│       ├── inference               
+│       ├── inference
 │       └── psi_fails               # Examples where Psi fails 
-├── evt_invariants                  # Synthesis of expected visiting time invariants
-├── independence                    # Independent variables
+├── equivalence                     # Equivalence of two programs
+│   ├── loop_free                   # Programs without loops and their counterparts
+│   └── loopy                       # Programs with loops
+│       └── invariants              # ... and their loop-free counterpart
+├── independence                    # Checks for independent variables
 ├── inference                       # Calculation of posterior distribution
 │   ├── loop_free                   # ... without while-loops
 │   │   └── conditioning            # ... with observe-statements
 │   └── loopy                       # ... with while-loops
 │       └── conditioning            # ... with observe-statements 
-├── loop_equivalence                # Equality of loopy and loop-free programs
-│   └── invariants                  # Corresponding loop-free programs
+├── invariant_synthesis             # Synthesis of (expected visiting time) invariants
 └── template_parameter_synthesis    # Equality of loopy and loop-free programs with parameters
-    └── invariants                  # Corresponding loop-free programs
- ```
\ No newline at end of file
+    └── invariants                  # Corresponding loop-free programs
+```
+
+## File structure
+
+* Files have a comment in the first line indicating which arguments should be used in order to execute it
+
+> ```bash
+>python prodigy/cli.py METHOD FILE ARGS 
+>```
+> results in
+>```
+># METHOD FILE ARGS
+>```
+> in the first line of the corresponding program or just
+> ```
+> # skip
+> ```
+> if the file should not be automatically tested.
+
+* Naming convention:
+    * In `pgfexamples/equivalence/loop_free` the files are named `file_name.pgcl` for the first and
+      `file_name2.pgcl` for the second program
+    * In `pgfexamples/equivalence/loopy` and `pgfexamples/template_parameter_synthesis` the files are named
+      `file_name.pgcl` in the main folder and their corresponding invariants with `file_name_invariant.pgcl` in the
+      invariants folder
+    * If there are multiple invariant files for one program, e.g. for a nested loop, the invariants are to be marked
+      with numbers indicating the order they should be used (i.e. the invariant for the outer-most while loop has number
+      1 and so on)
+    * Invariants and second programs are to be marked with `skip`
\ No newline at end of file
diff --git a/pgfexamples/equivalence/loop_free/bernoulli.pgcl b/pgfexamples/equivalence/loop_free/bernoulli.pgcl
new file mode 100644
index 0000000..0a3d2e3
--- /dev/null
+++ b/pgfexamples/equivalence/loop_free/bernoulli.pgcl
@@ -0,0 +1,4 @@
+# check_equality pgfexamples/equivalence/loop_free/bernoulli.pgcl pgfexamples/equivalence/loop_free/bernoulli2.pgcl
+nat x;
+
+{ x := 0 } [1/3] { x := 1 }
\ No newline at end of file
diff --git a/pgfexamples/equivalence/loop_free/bernoulli2.pgcl b/pgfexamples/equivalence/loop_free/bernoulli2.pgcl
new file mode 100644
index 0000000..17d24fd
--- /dev/null
+++ b/pgfexamples/equivalence/loop_free/bernoulli2.pgcl
@@ -0,0 +1,4 @@
+# skip
+nat x;
+
+x := bernoulli(2/3);
\ No newline at end of file
diff --git a/pgfexamples/equivalence/loop_free/dice_sampling.pgcl b/pgfexamples/equivalence/loop_free/dice_sampling.pgcl
new file mode 100644
index 0000000..8725265
--- /dev/null
+++ b/pgfexamples/equivalence/loop_free/dice_sampling.pgcl
@@ -0,0 +1,9 @@
+# check_equality pgfexamples/equivalence/loop_free/dice_sampling.pgcl pgfexamples/equivalence/loop_free/dice_sampling2.pgcl
+nat dice;
+nat tmp;
+
+tmp := 0;
+
+# Roll a dice
+dice := unif(1,6);
+
diff --git a/pgfexamples/equivalence/loop_free/dice_sampling2.pgcl b/pgfexamples/equivalence/loop_free/dice_sampling2.pgcl
new file mode 100644
index 0000000..bf248c5
--- /dev/null
+++ b/pgfexamples/equivalence/loop_free/dice_sampling2.pgcl
@@ -0,0 +1,11 @@
+# skip
+nat dice;
+nat tmp;
+
+# Roll a three-sided dice
+tmp := unif(1,3);
+
+# Flip a coin, leave or increase by 3
+{ dice := tmp; } [1/2] { dice := tmp + 3; }
+
+tmp := 0;
\ No newline at end of file
diff --git a/pgfexamples/equivalence/loop_free/uniform_sampling.pgcl b/pgfexamples/equivalence/loop_free/uniform_sampling.pgcl
new file mode 100644
index 0000000..34b31c3
--- /dev/null
+++ b/pgfexamples/equivalence/loop_free/uniform_sampling.pgcl
@@ -0,0 +1,4 @@
+# check_equality pgfexamples/equivalence/loop_free/uniform_sampling.pgcl pgfexamples/equivalence/loop_free/uniform_sampling2.pgcl
+nat x
+
+x := unif(1,6)
\ No newline at end of file
diff --git a/pgfexamples/equivalence/loop_free/uniform_sampling2.pgcl b/pgfexamples/equivalence/loop_free/uniform_sampling2.pgcl
new file mode 100644
index 0000000..f746fc5
--- /dev/null
+++ b/pgfexamples/equivalence/loop_free/uniform_sampling2.pgcl
@@ -0,0 +1,12 @@
+# skip
+nat x
+
+{x:=1}[1/6]{
+    {x:=2}[1/5]{
+        {x:=3}[1/4]{
+            {x:=4}[1/3]{
+                {x:=5}[1/2]{x:=6}
+            }
+        }
+    }
+}
\ No newline at end of file
diff --git a/pgfexamples/equivalence/loopy/17_die_even.pgcl b/pgfexamples/equivalence/loopy/17_die_even.pgcl
new file mode 100644
index 0000000..490a299
--- /dev/null
+++ b/pgfexamples/equivalence/loopy/17_die_even.pgcl
@@ -0,0 +1,11 @@
+# check_equality pgfexamples/equivalence/loopy/17_die_even.pgcl pgfexamples/equivalence/loopy/invariants/17_die_even_invariant.pgcl
+nat c
+nat x
+nat temp
+
+while (x < 6) {
+    x := unif(1,6)
+    c := c + 1
+    observe(x % 2 = 0)
+    temp := 0
+}
\ No newline at end of file
diff --git a/pgfexamples/loop_equivalence/bit_flip_conditioning.pgcl b/pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl
similarity index 58%
rename from pgfexamples/loop_equivalence/bit_flip_conditioning.pgcl
rename to pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl
index 784f9f1..51de045 100644
--- a/pgfexamples/loop_equivalence/bit_flip_conditioning.pgcl
+++ b/pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl
@@ -1,3 +1,4 @@
+# check_equality pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl pgfexamples/equivalence/loopy/invariants/bit_flip_conditioning_invariant.pgcl
 bool b1
 bool b2
 bool b3
@@ -5,7 +6,7 @@ bool b4
 nat i
 nat temp
 
-while (not ((b1 = 0) & (b2 = 0))) {
+while (b1=1 || b2=1) {
     b1 := bernoulli(1/2)
     b2 := bernoulli(1/2)
     observe( (b1 = 0 & b3 = 0) || (b1 = 1 & b3 = 1) || (b2 = 0 & b4 = 0) || (b2 = 1 & b4 = 1) )
diff --git a/pgfexamples/loop_equivalence/condand.pgcl b/pgfexamples/equivalence/loopy/condand.pgcl
similarity index 94%
rename from pgfexamples/loop_equivalence/condand.pgcl
rename to pgfexamples/equivalence/loopy/condand.pgcl
index f6cadad..cd83060 100644
--- a/pgfexamples/loop_equivalence/condand.pgcl
+++ b/pgfexamples/equivalence/loopy/condand.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat n;
 nat m;
 
diff --git a/pgfexamples/equivalence/loopy/dep_bern.pgcl b/pgfexamples/equivalence/loopy/dep_bern.pgcl
new file mode 100644
index 0000000..445675a
--- /dev/null
+++ b/pgfexamples/equivalence/loopy/dep_bern.pgcl
@@ -0,0 +1,12 @@
+# check_equality pgfexamples/equivalence/loopy/dep_bern.pgcl pgfexamples/equivalence/loopy/invariants/dep_bern_invariant.pgcl
+nat c;
+nat m;
+nat n;
+nat tmp;
+
+
+while( c > 0 ){
+    {m := m+1} [1/2] {n:= n+1}
+    c := c-1
+    tmp := 0
+}
diff --git a/pgfexamples/equivalence/loopy/endless_conditioning.pgcl b/pgfexamples/equivalence/loopy/endless_conditioning.pgcl
new file mode 100644
index 0000000..2da03ce
--- /dev/null
+++ b/pgfexamples/equivalence/loopy/endless_conditioning.pgcl
@@ -0,0 +1,7 @@
+# check_equality pgfexamples/equivalence/loopy/endless_conditioning.pgcl pgfexamples/equivalence/loopy/invariants/endless_conditioning_invariant.pgcl
+nat x;
+
+while(x=1){
+{x := 0}[1/2]{x:=1}
+observe(x=1)
+}
\ No newline at end of file
diff --git a/pgfexamples/equivalence/loopy/geometric.pgcl b/pgfexamples/equivalence/loopy/geometric.pgcl
new file mode 100644
index 0000000..a6f988e
--- /dev/null
+++ b/pgfexamples/equivalence/loopy/geometric.pgcl
@@ -0,0 +1,9 @@
+# check_equality pgfexamples/equivalence/loopy/geometric.pgcl pgfexamples/equivalence/loopy/invariants/geometric_invariant.pgcl
+nat x;
+nat c;
+nat temp;
+
+while (x = 1){
+ {x := 0 } [1/2] {c := c+1}
+ temp :=0
+}
\ No newline at end of file
diff --git a/pgfexamples/equivalence/loopy/geometric_observe.pgcl b/pgfexamples/equivalence/loopy/geometric_observe.pgcl
new file mode 100644
index 0000000..053ad20
--- /dev/null
+++ b/pgfexamples/equivalence/loopy/geometric_observe.pgcl
@@ -0,0 +1,11 @@
+# check_equality pgfexamples/equivalence/loopy/geometric_observe.pgcl pgfexamples/equivalence/loopy/invariants/geometric_observe_invariant.pgcl
+nat y;
+nat x;
+nat tmp;
+
+while ( y = 1){
+    {y := 0}[1/2]{y := 1};
+    x := x + 1;
+    observe( x < 3)
+    tmp := 0;
+}
\ No newline at end of file
diff --git a/pgfexamples/equivalence/loopy/geometric_shifted.pgcl b/pgfexamples/equivalence/loopy/geometric_shifted.pgcl
new file mode 100644
index 0000000..204bf33
--- /dev/null
+++ b/pgfexamples/equivalence/loopy/geometric_shifted.pgcl
@@ -0,0 +1,10 @@
+# check_equality pgfexamples/equivalence/loopy/geometric_shifted.pgcl pgfexamples/equivalence/loopy/invariants/geometric_shifted_invariant.pgcl
+nat x;
+nat c;
+nat temp;
+rparam p;
+
+while (x > 0){
+ {x := 0; c := c + 3 } [1/2] {c := c+1}
+ temp := 0
+}
\ No newline at end of file
diff --git a/pgfexamples/loop_equivalence/invariants/17_die_even_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/17_die_even_invariant.pgcl
similarity index 96%
rename from pgfexamples/loop_equivalence/invariants/17_die_even_invariant.pgcl
rename to pgfexamples/equivalence/loopy/invariants/17_die_even_invariant.pgcl
index 6ccf4cf..0adcd7a 100644
--- a/pgfexamples/loop_equivalence/invariants/17_die_even_invariant.pgcl
+++ b/pgfexamples/equivalence/loopy/invariants/17_die_even_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat c
 nat x
 nat temp
diff --git a/pgfexamples/loop_equivalence/invariants/bit_flip_conditioning_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/bit_flip_conditioning_invariant.pgcl
similarity index 98%
rename from pgfexamples/loop_equivalence/invariants/bit_flip_conditioning_invariant.pgcl
rename to pgfexamples/equivalence/loopy/invariants/bit_flip_conditioning_invariant.pgcl
index c3de1a9..f8e6abd 100644
--- a/pgfexamples/loop_equivalence/invariants/bit_flip_conditioning_invariant.pgcl
+++ b/pgfexamples/equivalence/loopy/invariants/bit_flip_conditioning_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 bool b1
 bool b2
 bool b3
diff --git a/pgfexamples/loop_equivalence/invariants/condand_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/condand_invariant.pgcl
similarity index 97%
rename from pgfexamples/loop_equivalence/invariants/condand_invariant.pgcl
rename to pgfexamples/equivalence/loopy/invariants/condand_invariant.pgcl
index a33c041..9e45b3a 100644
--- a/pgfexamples/loop_equivalence/invariants/condand_invariant.pgcl
+++ b/pgfexamples/equivalence/loopy/invariants/condand_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat n;
 nat m;
 
diff --git a/pgfexamples/loop_equivalence/invariants/dep_bern_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/dep_bern_invariant.pgcl
similarity index 97%
rename from pgfexamples/loop_equivalence/invariants/dep_bern_invariant.pgcl
rename to pgfexamples/equivalence/loopy/invariants/dep_bern_invariant.pgcl
index 353ff81..c82aa12 100644
--- a/pgfexamples/loop_equivalence/invariants/dep_bern_invariant.pgcl
+++ b/pgfexamples/equivalence/loopy/invariants/dep_bern_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat c;
 nat m;
 nat n;
diff --git a/pgfexamples/loop_equivalence/invariants/endless_conditioning_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/endless_conditioning_invariant.pgcl
similarity index 87%
rename from pgfexamples/loop_equivalence/invariants/endless_conditioning_invariant.pgcl
rename to pgfexamples/equivalence/loopy/invariants/endless_conditioning_invariant.pgcl
index 67eab4a..4a2fbaa 100644
--- a/pgfexamples/loop_equivalence/invariants/endless_conditioning_invariant.pgcl
+++ b/pgfexamples/equivalence/loopy/invariants/endless_conditioning_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat x;
 
 if (x = 1){
diff --git a/pgfexamples/loop_equivalence/invariants/geometric_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/geometric_invariant.pgcl
similarity index 94%
rename from pgfexamples/loop_equivalence/invariants/geometric_invariant.pgcl
rename to pgfexamples/equivalence/loopy/invariants/geometric_invariant.pgcl
index 6f09ba7..5f5d0b1 100644
--- a/pgfexamples/loop_equivalence/invariants/geometric_invariant.pgcl
+++ b/pgfexamples/equivalence/loopy/invariants/geometric_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat x;
 nat c;
 nat temp;
diff --git a/pgfexamples/loop_equivalence/geometric_observe_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/geometric_observe_invariant.pgcl
similarity index 95%
rename from pgfexamples/loop_equivalence/geometric_observe_invariant.pgcl
rename to pgfexamples/equivalence/loopy/invariants/geometric_observe_invariant.pgcl
index 26e3b0e..96c44b0 100644
--- a/pgfexamples/loop_equivalence/geometric_observe_invariant.pgcl
+++ b/pgfexamples/equivalence/loopy/invariants/geometric_observe_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat y;
 nat x;
 nat tmp;
diff --git a/pgfexamples/loop_equivalence/invariants/geometric_shifted_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/geometric_shifted_invariant.pgcl
similarity index 94%
rename from pgfexamples/loop_equivalence/invariants/geometric_shifted_invariant.pgcl
rename to pgfexamples/equivalence/loopy/invariants/geometric_shifted_invariant.pgcl
index 68a360a..480ddc3 100644
--- a/pgfexamples/loop_equivalence/invariants/geometric_shifted_invariant.pgcl
+++ b/pgfexamples/equivalence/loopy/invariants/geometric_shifted_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat x;
 nat c;
 nat temp;
diff --git a/pgfexamples/loop_equivalence/invariants/ky_die_2_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/ky_die_2_invariant.pgcl
similarity index 97%
rename from pgfexamples/loop_equivalence/invariants/ky_die_2_invariant.pgcl
rename to pgfexamples/equivalence/loopy/invariants/ky_die_2_invariant.pgcl
index 1af69cd..43fb190 100644
--- a/pgfexamples/loop_equivalence/invariants/ky_die_2_invariant.pgcl
+++ b/pgfexamples/equivalence/loopy/invariants/ky_die_2_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat s;
 nat die;
 
diff --git a/pgfexamples/loop_equivalence/invariants/ky_die_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/ky_die_invariant.pgcl
similarity index 99%
rename from pgfexamples/loop_equivalence/invariants/ky_die_invariant.pgcl
rename to pgfexamples/equivalence/loopy/invariants/ky_die_invariant.pgcl
index 0c79de0..d20a42b 100644
--- a/pgfexamples/loop_equivalence/invariants/ky_die_invariant.pgcl
+++ b/pgfexamples/equivalence/loopy/invariants/ky_die_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat s;
 nat die;
 
diff --git a/pgfexamples/loop_equivalence/invariants/n_geometric_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/n_geometric_invariant.pgcl
similarity index 94%
rename from pgfexamples/loop_equivalence/invariants/n_geometric_invariant.pgcl
rename to pgfexamples/equivalence/loopy/invariants/n_geometric_invariant.pgcl
index a17000b..3434b7f 100644
--- a/pgfexamples/loop_equivalence/invariants/n_geometric_invariant.pgcl
+++ b/pgfexamples/equivalence/loopy/invariants/n_geometric_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat n;
 nat c;
 nat tmp;
diff --git a/pgfexamples/loop_equivalence/invariants/nested_while_inv_outer.pgcl b/pgfexamples/equivalence/loopy/invariants/nested_while_invariant1.pgcl
similarity index 95%
rename from pgfexamples/loop_equivalence/invariants/nested_while_inv_outer.pgcl
rename to pgfexamples/equivalence/loopy/invariants/nested_while_invariant1.pgcl
index 372d86c..c0a6001 100644
--- a/pgfexamples/loop_equivalence/invariants/nested_while_inv_outer.pgcl
+++ b/pgfexamples/equivalence/loopy/invariants/nested_while_invariant1.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat x;
 nat y;
 nat c;
diff --git a/pgfexamples/loop_equivalence/invariants/nested_while_inv_inner.pgcl b/pgfexamples/equivalence/loopy/invariants/nested_while_invariant2.pgcl
similarity index 94%
rename from pgfexamples/loop_equivalence/invariants/nested_while_inv_inner.pgcl
rename to pgfexamples/equivalence/loopy/invariants/nested_while_invariant2.pgcl
index 50b138c..7accc56 100644
--- a/pgfexamples/loop_equivalence/invariants/nested_while_inv_inner.pgcl
+++ b/pgfexamples/equivalence/loopy/invariants/nested_while_invariant2.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat x;
 nat y;
 nat temp;
diff --git a/pgfexamples/loop_equivalence/invariants/random_walk_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/random_walk_invariant.pgcl
similarity index 95%
rename from pgfexamples/loop_equivalence/invariants/random_walk_invariant.pgcl
rename to pgfexamples/equivalence/loopy/invariants/random_walk_invariant.pgcl
index 3a5507f..0be24e5 100644
--- a/pgfexamples/loop_equivalence/invariants/random_walk_invariant.pgcl
+++ b/pgfexamples/equivalence/loopy/invariants/random_walk_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat s;
 nat c;
 nat tmp;
diff --git a/pgfexamples/loop_equivalence/invariants/rejection_sampling_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/rejection_sampling_invariant.pgcl
similarity index 91%
rename from pgfexamples/loop_equivalence/invariants/rejection_sampling_invariant.pgcl
rename to pgfexamples/equivalence/loopy/invariants/rejection_sampling_invariant.pgcl
index 79baad0..bbbd817 100644
--- a/pgfexamples/loop_equivalence/invariants/rejection_sampling_invariant.pgcl
+++ b/pgfexamples/equivalence/loopy/invariants/rejection_sampling_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat c;
 
 if(c%2=0){
diff --git a/pgfexamples/loop_equivalence/invariants/running_paper_example_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/running_paper_example_invariant.pgcl
similarity index 94%
rename from pgfexamples/loop_equivalence/invariants/running_paper_example_invariant.pgcl
rename to pgfexamples/equivalence/loopy/invariants/running_paper_example_invariant.pgcl
index 72812bb..4b0d4b9 100644
--- a/pgfexamples/loop_equivalence/invariants/running_paper_example_invariant.pgcl
+++ b/pgfexamples/equivalence/loopy/invariants/running_paper_example_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat x;
 nat c;
 nat tmp;
diff --git a/pgfexamples/loop_equivalence/invariants/sequential_loops_first_inv.pgcl b/pgfexamples/equivalence/loopy/invariants/sequential_loops_invariant1.pgcl
similarity index 94%
rename from pgfexamples/loop_equivalence/invariants/sequential_loops_first_inv.pgcl
rename to pgfexamples/equivalence/loopy/invariants/sequential_loops_invariant1.pgcl
index ca979cf..4dfada4 100644
--- a/pgfexamples/loop_equivalence/invariants/sequential_loops_first_inv.pgcl
+++ b/pgfexamples/equivalence/loopy/invariants/sequential_loops_invariant1.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat c;
 nat m;
 nat n;
diff --git a/pgfexamples/loop_equivalence/invariants/sequential_loops_second_inv.pgcl b/pgfexamples/equivalence/loopy/invariants/sequential_loops_invariant2.pgcl
similarity index 95%
rename from pgfexamples/loop_equivalence/invariants/sequential_loops_second_inv.pgcl
rename to pgfexamples/equivalence/loopy/invariants/sequential_loops_invariant2.pgcl
index ecdf9ec..ce43346 100644
--- a/pgfexamples/loop_equivalence/invariants/sequential_loops_second_inv.pgcl
+++ b/pgfexamples/equivalence/loopy/invariants/sequential_loops_invariant2.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat m;
 nat c;
 nat tmp;
diff --git a/pgfexamples/loop_equivalence/invariants/skip_rejection_sampling_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/skip_rejection_sampling_invariant.pgcl
similarity index 91%
rename from pgfexamples/loop_equivalence/invariants/skip_rejection_sampling_invariant.pgcl
rename to pgfexamples/equivalence/loopy/invariants/skip_rejection_sampling_invariant.pgcl
index b699236..e604e82 100644
--- a/pgfexamples/loop_equivalence/invariants/skip_rejection_sampling_invariant.pgcl
+++ b/pgfexamples/equivalence/loopy/invariants/skip_rejection_sampling_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat c;
 
 if ( not (c%2=0)){
diff --git a/pgfexamples/loop_equivalence/invariants/trivial_iid_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/trivial_iid_invariant.pgcl
similarity index 94%
rename from pgfexamples/loop_equivalence/invariants/trivial_iid_invariant.pgcl
rename to pgfexamples/equivalence/loopy/invariants/trivial_iid_invariant.pgcl
index 7abc1a1..c2cf3cd 100644
--- a/pgfexamples/loop_equivalence/invariants/trivial_iid_invariant.pgcl
+++ b/pgfexamples/equivalence/loopy/invariants/trivial_iid_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat n;
 nat m;
 nat tmp;
diff --git a/pgfexamples/loop_equivalence/ky_die.pgcl b/pgfexamples/equivalence/loopy/ky_die.pgcl
similarity index 88%
rename from pgfexamples/loop_equivalence/ky_die.pgcl
rename to pgfexamples/equivalence/loopy/ky_die.pgcl
index b9e51c0..7e13989 100644
--- a/pgfexamples/loop_equivalence/ky_die.pgcl
+++ b/pgfexamples/equivalence/loopy/ky_die.pgcl
@@ -1,3 +1,4 @@
+# check_equality pgfexamples/equivalence/loopy/ky_die.pgcl pgfexamples/equivalence/loopy/invariants/ky_die_invariant.pgcl
 nat s;
 nat die;
 
diff --git a/pgfexamples/loop_equivalence/ky_die_2.pgcl b/pgfexamples/equivalence/loopy/ky_die_2.pgcl
similarity index 73%
rename from pgfexamples/loop_equivalence/ky_die_2.pgcl
rename to pgfexamples/equivalence/loopy/ky_die_2.pgcl
index 90afe77..54f8d5b 100644
--- a/pgfexamples/loop_equivalence/ky_die_2.pgcl
+++ b/pgfexamples/equivalence/loopy/ky_die_2.pgcl
@@ -1,3 +1,4 @@
+# check_equality pgfexamples/equivalence/loopy/ky_die_2.pgcl pgfexamples/equivalence/loopy/invariants/ky_die_2_invariant.pgcl
 nat s;
 nat die;
 
diff --git a/pgfexamples/equivalence/loopy/n_geometric.pgcl b/pgfexamples/equivalence/loopy/n_geometric.pgcl
new file mode 100644
index 0000000..c909730
--- /dev/null
+++ b/pgfexamples/equivalence/loopy/n_geometric.pgcl
@@ -0,0 +1,9 @@
+# check_equality pgfexamples/equivalence/loopy/n_geometric.pgcl pgfexamples/equivalence/loopy/invariants/n_geometric_invariant.pgcl
+nat n;
+nat c;
+nat tmp;
+
+while(n > 0){
+    {n := n - 1 } [1/2] {c := c + 1}
+    tmp := 0
+}
\ No newline at end of file
diff --git a/pgfexamples/loop_equivalence/nested_while.pgcl b/pgfexamples/equivalence/loopy/nested_while.pgcl
similarity index 54%
rename from pgfexamples/loop_equivalence/nested_while.pgcl
rename to pgfexamples/equivalence/loopy/nested_while.pgcl
index ae8b084..17928c5 100644
--- a/pgfexamples/loop_equivalence/nested_while.pgcl
+++ b/pgfexamples/equivalence/loopy/nested_while.pgcl
@@ -1,3 +1,4 @@
+# check_equality pgfexamples/equivalence/loopy/nested_while.pgcl pgfexamples/equivalence/loopy/invariants/nested_while_invariant1.pgcl
 nat x;
 nat y;
 nat c;
diff --git a/pgfexamples/equivalence/loopy/random_walk.pgcl b/pgfexamples/equivalence/loopy/random_walk.pgcl
new file mode 100644
index 0000000..266b329
--- /dev/null
+++ b/pgfexamples/equivalence/loopy/random_walk.pgcl
@@ -0,0 +1,10 @@
+# check_equality pgfexamples/equivalence/loopy/random_walk.pgcl pgfexamples/equivalence/loopy/invariants/random_walk_invariant.pgcl
+nat s;
+nat c;
+nat tmp;
+
+while(s > 0){
+    {s := s+1} [1/2] {s := s-1}
+    c := c+1
+    tmp := 0
+}
\ No newline at end of file
diff --git a/pgfexamples/equivalence/loopy/running_paper_example.pgcl b/pgfexamples/equivalence/loopy/running_paper_example.pgcl
new file mode 100644
index 0000000..d20607c
--- /dev/null
+++ b/pgfexamples/equivalence/loopy/running_paper_example.pgcl
@@ -0,0 +1,9 @@
+# check_equality pgfexamples/equivalence/loopy/running_paper_example.pgcl pgfexamples/equivalence/loopy/invariants/running_paper_example_invariant.pgcl
+nat x;
+nat c;
+nat tmp;
+
+while(x > 0) {
+ { x := x-1 } [1/2] { c := c+1 }
+ tmp := 0;
+}
diff --git a/pgfexamples/loop_equivalence/sequential_loops.pgcl b/pgfexamples/equivalence/loopy/sequential_loops.pgcl
similarity index 55%
rename from pgfexamples/loop_equivalence/sequential_loops.pgcl
rename to pgfexamples/equivalence/loopy/sequential_loops.pgcl
index d9136da..1867d73 100644
--- a/pgfexamples/loop_equivalence/sequential_loops.pgcl
+++ b/pgfexamples/equivalence/loopy/sequential_loops.pgcl
@@ -1,3 +1,4 @@
+# check_equality pgfexamples/equivalence/loopy/sequential_loops.pgcl pgfexamples/equivalence/loopy/invariants/sequential_loops_invariant1.pgcl
 nat c;
 nat m;
 nat n;
diff --git a/pgfexamples/loop_equivalence/skip_rejection_sampling.pgcl b/pgfexamples/equivalence/loopy/skip_rejection_sampling.pgcl
similarity index 86%
rename from pgfexamples/loop_equivalence/skip_rejection_sampling.pgcl
rename to pgfexamples/equivalence/loopy/skip_rejection_sampling.pgcl
index fcd0e2c..8391271 100644
--- a/pgfexamples/loop_equivalence/skip_rejection_sampling.pgcl
+++ b/pgfexamples/equivalence/loopy/skip_rejection_sampling.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat c;
 
 while (c%2=0){
diff --git a/pgfexamples/equivalence/loopy/trivial_iid.pgcl b/pgfexamples/equivalence/loopy/trivial_iid.pgcl
new file mode 100644
index 0000000..871f817
--- /dev/null
+++ b/pgfexamples/equivalence/loopy/trivial_iid.pgcl
@@ -0,0 +1,12 @@
+# check_equality pgfexamples/equivalence/loopy/trivial_iid.pgcl pgfexamples/equivalence/loopy/invariants/trivial_iid_invariant.pgcl
+nat n;
+nat m;
+nat tmp;
+
+while (0 < n) {
+ tmp := unif(1,6);
+ m := m + tmp;
+ tmp := 0;
+ n := n-1
+}
+
diff --git a/pgfexamples/evt_invariants/faulty_decrement.pgcl b/pgfexamples/evt_invariants/faulty_decrement.pgcl
deleted file mode 100644
index f7d42e8..0000000
--- a/pgfexamples/evt_invariants/faulty_decrement.pgcl
+++ /dev/null
@@ -1,6 +0,0 @@
-nat x;
-
-x := geometric(1/2)
-while (x > 0){
-  {skip}[1/2]{x:=x-1}
-}
\ No newline at end of file
diff --git a/pgfexamples/evt_invariants/geometric.pgcl b/pgfexamples/evt_invariants/geometric.pgcl
deleted file mode 100644
index e011901..0000000
--- a/pgfexamples/evt_invariants/geometric.pgcl
+++ /dev/null
@@ -1,6 +0,0 @@
-nat x;
-
-x := 1
-while (x = 1){
- {x := 0} [1/2] {skip}
-}
\ No newline at end of file
diff --git a/pgfexamples/evt_invariants/geometric_counter.pgcl b/pgfexamples/evt_invariants/geometric_counter.pgcl
deleted file mode 100644
index 06e5d88..0000000
--- a/pgfexamples/evt_invariants/geometric_counter.pgcl
+++ /dev/null
@@ -1,7 +0,0 @@
-nat x;
-nat c;
-
-x := 1
-while (x = 1){
- {x := 0 } [1/2] {c := c+1}
-}
\ No newline at end of file
diff --git a/pgfexamples/evt_invariants/nontermination.pgcl b/pgfexamples/evt_invariants/nontermination.pgcl
deleted file mode 100644
index 49464c2..0000000
--- a/pgfexamples/evt_invariants/nontermination.pgcl
+++ /dev/null
@@ -1,6 +0,0 @@
-nat x;
-
-{x:=1}[1/2]{x:=2}
-while(x=1){
-  skip
-}
\ No newline at end of file
diff --git a/pgfexamples/evt_invariants/random_walk.pgcl b/pgfexamples/evt_invariants/random_walk.pgcl
deleted file mode 100644
index 88f72f9..0000000
--- a/pgfexamples/evt_invariants/random_walk.pgcl
+++ /dev/null
@@ -1,6 +0,0 @@
-nat x;
-
-x := 1
-while(x>0){
- {x:=x-1}[1/2]{x:=x+1}
-}
diff --git a/pgfexamples/evt_invariants/subdist_enter.pgcl b/pgfexamples/evt_invariants/subdist_enter.pgcl
deleted file mode 100644
index 726b258..0000000
--- a/pgfexamples/evt_invariants/subdist_enter.pgcl
+++ /dev/null
@@ -1,6 +0,0 @@
-nat x;
-
-{x:=1}[1/2]{x:=3}
-while (x > 2){
-  {skip}[1/2]{x:=x-1}
-}
\ No newline at end of file
diff --git a/pgfexamples/independence/infinite_multiplication.pgcl b/pgfexamples/independence/infinite_multiplication.pgcl
index f33e6f4..677af4a 100644
--- a/pgfexamples/independence/infinite_multiplication.pgcl
+++ b/pgfexamples/independence/infinite_multiplication.pgcl
@@ -1,3 +1,5 @@
+# skip
+# fails (on purpose)
 nat x;
 nat y;
 nat z;
diff --git a/pgfexamples/independence/oblivious_transfer.pgcl b/pgfexamples/independence/oblivious_transfer.pgcl
index 3396334..2340186 100644
--- a/pgfexamples/independence/oblivious_transfer.pgcl
+++ b/pgfexamples/independence/oblivious_transfer.pgcl
@@ -1,3 +1,4 @@
+
 # 3 bit messages, no real bitwise XOR used, inspirited by Barthe et al., A Probabilistic Separation Logic
 
 nat r0;
diff --git a/pgfexamples/independence/private_information_retriveal.pgcl b/pgfexamples/independence/private_information_retriveal.pgcl
index 136f687..9d7c534 100644
--- a/pgfexamples/independence/private_information_retriveal.pgcl
+++ b/pgfexamples/independence/private_information_retriveal.pgcl
@@ -1,3 +1,4 @@
+
 # 3 bit, bitwise, inspirited by Barthe et al., A Probabilistic Separation Logic
 
 nat q00;
diff --git a/pgfexamples/inference/loop_free/conditioning/burgler_alarm.pgcl b/pgfexamples/inference/loop_free/conditioning/burgler_alarm.pgcl
index 18a932e..6eaea6a 100644
--- a/pgfexamples/inference/loop_free/conditioning/burgler_alarm.pgcl
+++ b/pgfexamples/inference/loop_free/conditioning/burgler_alarm.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/conditioning/burgler_alarm.pgcl
 nat earthquake;
 nat burglary;
 nat alarm;
diff --git a/pgfexamples/inference/loop_free/conditioning/caesar.pgcl b/pgfexamples/inference/loop_free/conditioning/caesar.pgcl
index aaca59b..a787d66 100644
--- a/pgfexamples/inference/loop_free/conditioning/caesar.pgcl
+++ b/pgfexamples/inference/loop_free/conditioning/caesar.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/conditioning/caesar.pgcl
 nat key;
 nat randomChar;
 nat cipher;
diff --git a/pgfexamples/inference/loop_free/conditioning/conditioning_divergence.pgcl b/pgfexamples/inference/loop_free/conditioning/conditioning_divergence.pgcl
index d49d87c..29816d6 100644
--- a/pgfexamples/inference/loop_free/conditioning/conditioning_divergence.pgcl
+++ b/pgfexamples/inference/loop_free/conditioning/conditioning_divergence.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/conditioning/conditioning_divergence.pgcl
 nat x;
 nat y;
 
diff --git a/pgfexamples/inference/loop_free/conditioning/digitRecognition.pgcl b/pgfexamples/inference/loop_free/conditioning/digitRecognition.pgcl
index a85c580..8abcec5 100644
--- a/pgfexamples/inference/loop_free/conditioning/digitRecognition.pgcl
+++ b/pgfexamples/inference/loop_free/conditioning/digitRecognition.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/conditioning/digitRecognition.pgcl
 nat y;
 nat tmp;
 
diff --git a/pgfexamples/inference/loop_free/conditioning/evidence1.pgcl b/pgfexamples/inference/loop_free/conditioning/evidence1.pgcl
index 77c8ef2..39da5e1 100644
--- a/pgfexamples/inference/loop_free/conditioning/evidence1.pgcl
+++ b/pgfexamples/inference/loop_free/conditioning/evidence1.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/conditioning/evidence1.pgcl
 nat evidence;
 nat coin;
 
diff --git a/pgfexamples/inference/loop_free/conditioning/evidence2.pgcl b/pgfexamples/inference/loop_free/conditioning/evidence2.pgcl
index 23e83bf..a1c71fc 100644
--- a/pgfexamples/inference/loop_free/conditioning/evidence2.pgcl
+++ b/pgfexamples/inference/loop_free/conditioning/evidence2.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/conditioning/evidence2.pgcl
 nat evidence;
 nat coin;
 nat coin1;
diff --git a/pgfexamples/inference/loop_free/conditioning/grass.pgcl b/pgfexamples/inference/loop_free/conditioning/grass.pgcl
index 3248ffe..b23a8f2 100644
--- a/pgfexamples/inference/loop_free/conditioning/grass.pgcl
+++ b/pgfexamples/inference/loop_free/conditioning/grass.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/conditioning/grass.pgcl
 nat cloudy;
 nat rain;
 nat sprinkler;
diff --git a/pgfexamples/inference/loop_free/conditioning/infer_geom_mix.pgcl b/pgfexamples/inference/loop_free/conditioning/infer_geom_mix.pgcl
index e7d5daf..9b90887 100644
--- a/pgfexamples/inference/loop_free/conditioning/infer_geom_mix.pgcl
+++ b/pgfexamples/inference/loop_free/conditioning/infer_geom_mix.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/conditioning/infer_geom_mix.pgcl
 // sample from either 1, 2, or 3 geom distributions and add the results
 // infer from how many distributions we sampled based on observing one result
 
diff --git a/pgfexamples/inference/loop_free/conditioning/lin_regression_unbiased.pgcl b/pgfexamples/inference/loop_free/conditioning/lin_regression_unbiased.pgcl
index 6f56988..e3bd8b9 100644
--- a/pgfexamples/inference/loop_free/conditioning/lin_regression_unbiased.pgcl
+++ b/pgfexamples/inference/loop_free/conditioning/lin_regression_unbiased.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/conditioning/lin_regression_unbiased.pgcl
 nat a;
 nat b;
 nat x1;
diff --git a/pgfexamples/inference/loop_free/conditioning/lucky_throw.pgcl b/pgfexamples/inference/loop_free/conditioning/lucky_throw.pgcl
index 3ec7902..2c0a2cc 100644
--- a/pgfexamples/inference/loop_free/conditioning/lucky_throw.pgcl
+++ b/pgfexamples/inference/loop_free/conditioning/lucky_throw.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/conditioning/lucky_throw.pgcl
 nat die;
 nat lucky_throw;
 nat hand;
diff --git a/pgfexamples/inference/loop_free/conditioning/monty_hall_nested.pgcl b/pgfexamples/inference/loop_free/conditioning/monty_hall_nested.pgcl
index 759bdc0..b7c9dab 100644
--- a/pgfexamples/inference/loop_free/conditioning/monty_hall_nested.pgcl
+++ b/pgfexamples/inference/loop_free/conditioning/monty_hall_nested.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/conditioning/monty_hall_nested.pgcl
 nat prize;
 nat player;
 nat door;
diff --git a/pgfexamples/inference/loop_free/conditioning/murder_mystery.pgcl b/pgfexamples/inference/loop_free/conditioning/murder_mystery.pgcl
index e13ecce..c348ead 100644
--- a/pgfexamples/inference/loop_free/conditioning/murder_mystery.pgcl
+++ b/pgfexamples/inference/loop_free/conditioning/murder_mystery.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/conditioning/murder_mystery.pgcl
 nat aliceDunnit;
 nat withGun;
 rparam p;
diff --git a/pgfexamples/inference/loop_free/conditioning/skip_lin_regression_biased.pgcl b/pgfexamples/inference/loop_free/conditioning/skip_lin_regression_biased.pgcl
index 9ea3980..83de75c 100644
--- a/pgfexamples/inference/loop_free/conditioning/skip_lin_regression_biased.pgcl
+++ b/pgfexamples/inference/loop_free/conditioning/skip_lin_regression_biased.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat a;
 nat b;
 nat x1;
diff --git a/pgfexamples/inference/loop_free/conditioning/telephone_operator.pgcl b/pgfexamples/inference/loop_free/conditioning/telephone_operator.pgcl
index 9b6ce2a..e72700e 100644
--- a/pgfexamples/inference/loop_free/conditioning/telephone_operator.pgcl
+++ b/pgfexamples/inference/loop_free/conditioning/telephone_operator.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/conditioning/telephone_operator.pgcl
 nat x; // 0: weekday, 1: weekend
 nat d; // sample the number of phone calls received in one hour.
 //rparam p;
diff --git a/pgfexamples/inference/loop_free/conditioning/twocoins.pgcl b/pgfexamples/inference/loop_free/conditioning/twocoins.pgcl
index e041ed8..1725bb7 100644
--- a/pgfexamples/inference/loop_free/conditioning/twocoins.pgcl
+++ b/pgfexamples/inference/loop_free/conditioning/twocoins.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/conditioning/twocoins.pgcl
 nat firstCoin;
 nat secondCoin;
 nat bothHeads;
diff --git a/pgfexamples/inference/loop_free/conditioning/undefined_normalization.pgcl b/pgfexamples/inference/loop_free/conditioning/undefined_normalization.pgcl
index cfeb2dd..41d587f 100644
--- a/pgfexamples/inference/loop_free/conditioning/undefined_normalization.pgcl
+++ b/pgfexamples/inference/loop_free/conditioning/undefined_normalization.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/conditioning/undefined_normalization.pgcl
 nat x;
 
 observe(false)
\ No newline at end of file
diff --git a/pgfexamples/inference/loop_free/dnd_handicap.pgcl b/pgfexamples/inference/loop_free/dnd_handicap.pgcl
index c649b49..c0c5937 100644
--- a/pgfexamples/inference/loop_free/dnd_handicap.pgcl
+++ b/pgfexamples/inference/loop_free/dnd_handicap.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/dnd_handicap.pgcl
 // Estimates benefits or punishments when beeing allowed to throw multiple dice
 // and take the maximum / mininmum of these dice. The punishment is controlled
 // by the variable `good`.
diff --git a/pgfexamples/inference/loop_free/function.pgcl b/pgfexamples/inference/loop_free/function.pgcl
index fb90f56..85a65b0 100644
--- a/pgfexamples/inference/loop_free/function.pgcl
+++ b/pgfexamples/inference/loop_free/function.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/function.pgcl
 fun f := {
     nat a;
     return 20*a + 2;
diff --git a/pgfexamples/inference/loop_free/fuzzy_or.pgcl b/pgfexamples/inference/loop_free/fuzzy_or.pgcl
index f4d2c42..9fb3b1e 100644
--- a/pgfexamples/inference/loop_free/fuzzy_or.pgcl
+++ b/pgfexamples/inference/loop_free/fuzzy_or.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/fuzzy_or.pgcl
 nat n0;
 nat n1;
 nat n2;
diff --git a/pgfexamples/inference/loop_free/max.pgcl b/pgfexamples/inference/loop_free/max.pgcl
index c480973..7c15875 100644
--- a/pgfexamples/inference/loop_free/max.pgcl
+++ b/pgfexamples/inference/loop_free/max.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/max.pgcl
 fun max := {
     nat x;
     nat y;
diff --git a/pgfexamples/inference/loop_free/monty_hall.pgcl b/pgfexamples/inference/loop_free/monty_hall.pgcl
index 8cc9254..e2ae780 100644
--- a/pgfexamples/inference/loop_free/monty_hall.pgcl
+++ b/pgfexamples/inference/loop_free/monty_hall.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/monty_hall.pgcl
 nat prize;
 nat player;
 nat opendoor;
diff --git a/pgfexamples/inference/loop_free/pi.pgcl b/pgfexamples/inference/loop_free/pi.pgcl
index c35b2fa..4254e8c 100644
--- a/pgfexamples/inference/loop_free/pi.pgcl
+++ b/pgfexamples/inference/loop_free/pi.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/pi.pgcl
 nat x
 nat y
 x := unif(0,30)
diff --git a/pgfexamples/inference/loop_free/piranha.pgcl b/pgfexamples/inference/loop_free/piranha.pgcl
index 4987f1c..11ef4dd 100644
--- a/pgfexamples/inference/loop_free/piranha.pgcl
+++ b/pgfexamples/inference/loop_free/piranha.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/piranha.pgcl
 nat piranha
 nat fish_taken_is_piranha
 
diff --git a/pgfexamples/inference/loop_free/poor_scale.pgcl b/pgfexamples/inference/loop_free/poor_scale.pgcl
index 4298df0..98e9ff5 100644
--- a/pgfexamples/inference/loop_free/poor_scale.pgcl
+++ b/pgfexamples/inference/loop_free/poor_scale.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/poor_scale.pgcl
 nat n;
 nat x;
 
diff --git a/pgfexamples/inference/loop_free/prob_collatz.pgcl b/pgfexamples/inference/loop_free/prob_collatz.pgcl
index 14dc157..a3c06f0 100644
--- a/pgfexamples/inference/loop_free/prob_collatz.pgcl
+++ b/pgfexamples/inference/loop_free/prob_collatz.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/prob_collatz.pgcl
 nat n;
 nat x;
 
diff --git a/pgfexamples/inference/loop_free/scalability.pgcl b/pgfexamples/inference/loop_free/scalability.pgcl
index 9aaa0f2..273729a 100644
--- a/pgfexamples/inference/loop_free/scalability.pgcl
+++ b/pgfexamples/inference/loop_free/scalability.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loop_free/scalability.pgcl
 nat x;
 
 x := geometric(1/2);
diff --git a/pgfexamples/inference/loopy/conditioning/dep_bern.pgcl b/pgfexamples/inference/loopy/conditioning/dep_bern.pgcl
index a4cf45a..ef3083c 100644
--- a/pgfexamples/inference/loopy/conditioning/dep_bern.pgcl
+++ b/pgfexamples/inference/loopy/conditioning/dep_bern.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loopy/conditioning/dep_bern.pgcl
 nat c;
 nat m;
 nat n;
diff --git a/pgfexamples/inference/loopy/conditioning/trivial_iid.pgcl b/pgfexamples/inference/loopy/conditioning/trivial_iid.pgcl
index 313d80c..8e0124f 100644
--- a/pgfexamples/inference/loopy/conditioning/trivial_iid.pgcl
+++ b/pgfexamples/inference/loopy/conditioning/trivial_iid.pgcl
@@ -1,3 +1,4 @@
+# main pgfexamples/inference/loopy/conditioning/trivial_iid.pgcl
 nat n;
 nat m;
 nat tmp;
diff --git a/pgfexamples/inference/loopy/skip_exceeding_sum.pgcl b/pgfexamples/inference/loopy/skip_exceeding_sum.pgcl
index 95a22e5..2e19ad9 100644
--- a/pgfexamples/inference/loopy/skip_exceeding_sum.pgcl
+++ b/pgfexamples/inference/loopy/skip_exceeding_sum.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat sum;
 nat c;
 nat temp;
diff --git a/pgfexamples/inference/loopy/skip_geom_dist.pgcl b/pgfexamples/inference/loopy/skip_geom_dist.pgcl
index c80656b..1460d83 100644
--- a/pgfexamples/inference/loopy/skip_geom_dist.pgcl
+++ b/pgfexamples/inference/loopy/skip_geom_dist.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat x;
 nat c;
 
diff --git a/pgfexamples/inference/loopy/skip_random_walk.pgcl b/pgfexamples/inference/loopy/skip_random_walk.pgcl
index 5d1fe5f..3079269 100644
--- a/pgfexamples/inference/loopy/skip_random_walk.pgcl
+++ b/pgfexamples/inference/loopy/skip_random_walk.pgcl
@@ -1,3 +1,4 @@
+# skip
 // Currently leads to issues!
 
 nat x;
diff --git a/pgfexamples/inference/loopy/uniform_sampling.pgcl b/pgfexamples/inference/loopy/uniform_sampling.pgcl
index 3f2181f..2b1f846 100644
--- a/pgfexamples/inference/loopy/uniform_sampling.pgcl
+++ b/pgfexamples/inference/loopy/uniform_sampling.pgcl
@@ -1,6 +1,7 @@
+# main pgfexamples/inference/loopy/uniform_sampling.pgcl
+# TODO How to choose option
 # correctness proof in [Lumbroso 2013]
 # invariant most likely not in loop-free ReDiP-Fragment.
-
 nat running;
 nat v;
 nat c;
diff --git a/pgfexamples/evt_invariants/cond_and.pgcl b/pgfexamples/invariant_synthesis/cond_and.pgcl
similarity index 52%
rename from pgfexamples/evt_invariants/cond_and.pgcl
rename to pgfexamples/invariant_synthesis/cond_and.pgcl
index 06b8c67..65155f6 100644
--- a/pgfexamples/evt_invariants/cond_and.pgcl
+++ b/pgfexamples/invariant_synthesis/cond_and.pgcl
@@ -1,3 +1,4 @@
+# invariant_synthesis pgfexamples/invariant_synthesis/cond_and.pgcl
 nat m;
 nat n;
 
diff --git a/pgfexamples/inference/loopy/dueling_cowboys.pgcl b/pgfexamples/invariant_synthesis/dueling_cowboys.pgcl
similarity index 84%
rename from pgfexamples/inference/loopy/dueling_cowboys.pgcl
rename to pgfexamples/invariant_synthesis/dueling_cowboys.pgcl
index d785937..66c89db 100644
--- a/pgfexamples/inference/loopy/dueling_cowboys.pgcl
+++ b/pgfexamples/invariant_synthesis/dueling_cowboys.pgcl
@@ -1,3 +1,4 @@
+# invariant_synthesis pgfexamples/invariant_synthesis/dueling_cowboys.pgcl
 nat t; // t = 0 player A's turn; t = 1 player B's turn; t>1 not interpretable
 nat c; // c=1, both player alive; c = 0 one player dead; c>1 not interpretable
 rparam a; // probability that Player A shoots player B in a turn.
diff --git a/pgfexamples/evt_invariants/fast_dice_roller.pgcl b/pgfexamples/invariant_synthesis/fast_dice_roller.pgcl
similarity index 91%
rename from pgfexamples/evt_invariants/fast_dice_roller.pgcl
rename to pgfexamples/invariant_synthesis/fast_dice_roller.pgcl
index 7954b21..9faaed2 100644
--- a/pgfexamples/evt_invariants/fast_dice_roller.pgcl
+++ b/pgfexamples/invariant_synthesis/fast_dice_roller.pgcl
@@ -1,3 +1,4 @@
+# invariant_synthesis pgfexamples/invariant_synthesis/fast_dice_roller.pgcl
 nat v;
 nat c;
 bool flag;
@@ -21,7 +22,7 @@ while (flag = 0) {
 
 flag := 0
 v := 0
-!Plot[c, \infty]
+#!Plot[c, \infty]
 
 // Invariant template seems to be: a*v^4*flag*(1+c+c^2)+b*v^2*(1+c)+d*v with solution: [{a: 1/3, b: 2/3, d: 4/3}]
 
diff --git a/pgfexamples/invariant_synthesis/faulty_decrement.pgcl b/pgfexamples/invariant_synthesis/faulty_decrement.pgcl
new file mode 100644
index 0000000..4aeed3c
--- /dev/null
+++ b/pgfexamples/invariant_synthesis/faulty_decrement.pgcl
@@ -0,0 +1,7 @@
+# invariant_synthesis pgfexamples/invariant_synthesis/faulty_decrement.pgcl
+nat x;
+
+x := geometric(1/2)
+while (x > 0){
+  {skip}[1/2]{x:=x-1}
+}
\ No newline at end of file
diff --git a/pgfexamples/invariant_synthesis/geometric.pgcl b/pgfexamples/invariant_synthesis/geometric.pgcl
new file mode 100644
index 0000000..f66f954
--- /dev/null
+++ b/pgfexamples/invariant_synthesis/geometric.pgcl
@@ -0,0 +1,7 @@
+# invariant_synthesis pgfexamples/invariant_synthesis/geometric.pgcl
+nat x;
+
+x := 1
+while (x = 1){
+ {x := 0} [1/2] {skip}
+}
\ No newline at end of file
diff --git a/pgfexamples/invariant_synthesis/geometric_counter.pgcl b/pgfexamples/invariant_synthesis/geometric_counter.pgcl
new file mode 100644
index 0000000..38b095c
--- /dev/null
+++ b/pgfexamples/invariant_synthesis/geometric_counter.pgcl
@@ -0,0 +1,8 @@
+# invariant_synthesis pgfexamples/invariant_synthesis/geometric_counter.pgcl
+nat x;
+nat c;
+
+x := 1
+while (x = 1){
+ {x := 0 } [1/2] {c := c+1}
+}
\ No newline at end of file
diff --git a/pgfexamples/evt_invariants/modulo_geometric.pgcl b/pgfexamples/invariant_synthesis/modulo_geometric.pgcl
similarity index 68%
rename from pgfexamples/evt_invariants/modulo_geometric.pgcl
rename to pgfexamples/invariant_synthesis/modulo_geometric.pgcl
index 7922e91..44ad390 100644
--- a/pgfexamples/evt_invariants/modulo_geometric.pgcl
+++ b/pgfexamples/invariant_synthesis/modulo_geometric.pgcl
@@ -1,3 +1,4 @@
+# invariant_synthesis pgfexamples/invariant_synthesis/modulo_geometric.pgcl
 nat x;
 
 x := geometric(1/2)
diff --git a/pgfexamples/invariant_synthesis/nontermination.pgcl b/pgfexamples/invariant_synthesis/nontermination.pgcl
new file mode 100644
index 0000000..645c90f
--- /dev/null
+++ b/pgfexamples/invariant_synthesis/nontermination.pgcl
@@ -0,0 +1,8 @@
+# skip
+# --solver z3 invariant_synthesis pgfexamples/invariant_synthesis/nontermination.pgcl
+nat x;
+
+{x:=1}[1/2]{x:=2}
+while(x=1){
+  skip
+}
\ No newline at end of file
diff --git a/pgfexamples/invariant_synthesis/random_walk.pgcl b/pgfexamples/invariant_synthesis/random_walk.pgcl
new file mode 100644
index 0000000..9334be1
--- /dev/null
+++ b/pgfexamples/invariant_synthesis/random_walk.pgcl
@@ -0,0 +1,7 @@
+# invariant_synthesis pgfexamples/invariant_synthesis/random_walk.pgcl
+nat x;
+
+x := 1
+while(x>0){
+ {x:=x-1}[1/2]{x:=x+1}
+}
diff --git a/pgfexamples/evt_invariants/skip_random_walk_counter.pgcl b/pgfexamples/invariant_synthesis/skip_random_walk_counter.pgcl
similarity index 96%
rename from pgfexamples/evt_invariants/skip_random_walk_counter.pgcl
rename to pgfexamples/invariant_synthesis/skip_random_walk_counter.pgcl
index 7a3a11e..32d099b 100644
--- a/pgfexamples/evt_invariants/skip_random_walk_counter.pgcl
+++ b/pgfexamples/invariant_synthesis/skip_random_walk_counter.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat x;
 nat c;
 
diff --git a/pgfexamples/evt_invariants/skip_sequential_loops.pgcl b/pgfexamples/invariant_synthesis/skip_sequential_loops.pgcl
similarity index 94%
rename from pgfexamples/evt_invariants/skip_sequential_loops.pgcl
rename to pgfexamples/invariant_synthesis/skip_sequential_loops.pgcl
index d3c1942..a83a446 100644
--- a/pgfexamples/evt_invariants/skip_sequential_loops.pgcl
+++ b/pgfexamples/invariant_synthesis/skip_sequential_loops.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat x;
 nat c;
 
diff --git a/pgfexamples/invariant_synthesis/subdist_enter.pgcl b/pgfexamples/invariant_synthesis/subdist_enter.pgcl
new file mode 100644
index 0000000..ac4dca8
--- /dev/null
+++ b/pgfexamples/invariant_synthesis/subdist_enter.pgcl
@@ -0,0 +1,7 @@
+# invariant_synthesis pgfexamples/invariant_synthesis/subdist_enter.pgcl
+nat x;
+
+{x:=1}[1/2]{x:=3}
+while (x > 2){
+  {skip}[1/2]{x:=x-1}
+}
\ No newline at end of file
diff --git a/pgfexamples/evt_invariants/thirds_geometric.pgcl b/pgfexamples/invariant_synthesis/thirds_geometric.pgcl
similarity index 87%
rename from pgfexamples/evt_invariants/thirds_geometric.pgcl
rename to pgfexamples/invariant_synthesis/thirds_geometric.pgcl
index a8c3ac1..6a4834b 100644
--- a/pgfexamples/evt_invariants/thirds_geometric.pgcl
+++ b/pgfexamples/invariant_synthesis/thirds_geometric.pgcl
@@ -1,3 +1,4 @@
+# invariant_synthesis pgfexamples/invariant_synthesis/thirds_geometric.pgcl
 nat x;
 
 x := 1
diff --git a/pgfexamples/loop_equivalence/17_die_even.pgcl b/pgfexamples/loop_equivalence/17_die_even.pgcl
deleted file mode 100644
index 7a60dc3..0000000
--- a/pgfexamples/loop_equivalence/17_die_even.pgcl
+++ /dev/null
@@ -1,10 +0,0 @@
-nat c
-nat x
-nat temp
-
-while (x < 6) {
-    x := unif(1,6)
-    c := c + 1
-    observe(x % 2 = 0)
-    temp := 0
-}
\ No newline at end of file
diff --git a/pgfexamples/loop_equivalence/dep_bern.pgcl b/pgfexamples/loop_equivalence/dep_bern.pgcl
deleted file mode 100644
index d6bdac7..0000000
--- a/pgfexamples/loop_equivalence/dep_bern.pgcl
+++ /dev/null
@@ -1,11 +0,0 @@
-nat c;
-nat m;
-nat n;
-nat tmp;
-
-
-while( c > 0 ){
-    {m := m+1} [1/2] {n:= n+1}
-    c := c-1
-    tmp := 0
-}
diff --git a/pgfexamples/loop_equivalence/endless_conditioning.pgcl b/pgfexamples/loop_equivalence/endless_conditioning.pgcl
deleted file mode 100644
index eafd35a..0000000
--- a/pgfexamples/loop_equivalence/endless_conditioning.pgcl
+++ /dev/null
@@ -1,7 +0,0 @@
-
-nat x;
-
-while(x=1){
-{x := 0}[1/2]{x:=1}
-observe(x=1)
-}
\ No newline at end of file
diff --git a/pgfexamples/loop_equivalence/geometric.pgcl b/pgfexamples/loop_equivalence/geometric.pgcl
deleted file mode 100644
index 41346f6..0000000
--- a/pgfexamples/loop_equivalence/geometric.pgcl
+++ /dev/null
@@ -1,8 +0,0 @@
-nat x;
-nat c;
-nat temp;
-
-while (x = 1){
- {x := 0 } [1/2] {c := c+1}
- temp :=0
-}
\ No newline at end of file
diff --git a/pgfexamples/loop_equivalence/geometric_observe.pgcl b/pgfexamples/loop_equivalence/geometric_observe.pgcl
deleted file mode 100644
index 00afd7f..0000000
--- a/pgfexamples/loop_equivalence/geometric_observe.pgcl
+++ /dev/null
@@ -1,10 +0,0 @@
-nat y;
-nat x;
-nat tmp;
-
-while ( y = 1){
-    {y := 0}[1/2]{y := 1};
-    x := x + 1;
-    observe( x < 3)
-    tmp := 0;
-}
\ No newline at end of file
diff --git a/pgfexamples/loop_equivalence/geometric_shifted.pgcl b/pgfexamples/loop_equivalence/geometric_shifted.pgcl
deleted file mode 100644
index a0b61ea..0000000
--- a/pgfexamples/loop_equivalence/geometric_shifted.pgcl
+++ /dev/null
@@ -1,9 +0,0 @@
-nat x;
-nat c;
-nat temp;
-rparam p;
-
-while (x > 0){
- {x := 0; c := c + 3 } [1/2] {c := c+1}
- temp := 0
-}
\ No newline at end of file
diff --git a/pgfexamples/loop_equivalence/n_geometric.pgcl b/pgfexamples/loop_equivalence/n_geometric.pgcl
deleted file mode 100644
index e1e29c9..0000000
--- a/pgfexamples/loop_equivalence/n_geometric.pgcl
+++ /dev/null
@@ -1,8 +0,0 @@
-nat n;
-nat c;
-nat tmp;
-
-while(n > 0){
-    {n := n - 1 } [1/2] {c := c + 1}
-    tmp := 0
-}
\ No newline at end of file
diff --git a/pgfexamples/loop_equivalence/random_walk.pgcl b/pgfexamples/loop_equivalence/random_walk.pgcl
deleted file mode 100644
index f3533eb..0000000
--- a/pgfexamples/loop_equivalence/random_walk.pgcl
+++ /dev/null
@@ -1,9 +0,0 @@
-nat s;
-nat c;
-nat tmp;
-
-while(s > 0){
-    {s := s+1} [1/2] {s := s-1}
-    c := c+1
-    tmp := 0
-}
\ No newline at end of file
diff --git a/pgfexamples/loop_equivalence/running_paper_example.pgcl b/pgfexamples/loop_equivalence/running_paper_example.pgcl
deleted file mode 100644
index cd70bd6..0000000
--- a/pgfexamples/loop_equivalence/running_paper_example.pgcl
+++ /dev/null
@@ -1,8 +0,0 @@
-nat x;
-nat c;
-nat tmp;
-
-while(x > 0) {
- { x := x-1 } [1/2] { c := c+1 }
- tmp := 0;
-}
diff --git a/pgfexamples/loop_equivalence/trivial_iid.pgcl b/pgfexamples/loop_equivalence/trivial_iid.pgcl
deleted file mode 100644
index 7e4770b..0000000
--- a/pgfexamples/loop_equivalence/trivial_iid.pgcl
+++ /dev/null
@@ -1,11 +0,0 @@
-nat n;
-nat m;
-nat tmp;
-
-while (0 < n) {
- tmp := unif(1,6);
- m := m + tmp;
- tmp := 0;
- n := n-1
-}
-
diff --git a/pgfexamples/template_parameter_synthesis/bit_flip_conditioning_generalized_parameter.pgcl b/pgfexamples/template_parameter_synthesis/bit_flip_conditioning_generalized_parameter.pgcl
index 599a593..bca9394 100644
--- a/pgfexamples/template_parameter_synthesis/bit_flip_conditioning_generalized_parameter.pgcl
+++ b/pgfexamples/template_parameter_synthesis/bit_flip_conditioning_generalized_parameter.pgcl
@@ -1,3 +1,4 @@
+# check_equality pgfexamples/template_parameter_synthesis/bit_flip_conditioning_generalized_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/bit_flip_conditioning_generalized_parameter_invariant.pgcl
 bool b1
 bool b2
 bool b3
diff --git a/pgfexamples/template_parameter_synthesis/bit_flip_conditioning_parameter.pgcl b/pgfexamples/template_parameter_synthesis/bit_flip_conditioning_parameter.pgcl
index 784f9f1..a1eff73 100644
--- a/pgfexamples/template_parameter_synthesis/bit_flip_conditioning_parameter.pgcl
+++ b/pgfexamples/template_parameter_synthesis/bit_flip_conditioning_parameter.pgcl
@@ -1,3 +1,4 @@
+# check_equality pgfexamples/template_parameter_synthesis/bit_flip_conditioning_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/bit_flip_conditioning_parameter_invariant.pgcl
 bool b1
 bool b2
 bool b3
diff --git a/pgfexamples/template_parameter_synthesis/brp_obs_parameter.pgcl b/pgfexamples/template_parameter_synthesis/brp_obs_parameter.pgcl
index f859b98..d40d052 100644
--- a/pgfexamples/template_parameter_synthesis/brp_obs_parameter.pgcl
+++ b/pgfexamples/template_parameter_synthesis/brp_obs_parameter.pgcl
@@ -1,3 +1,4 @@
+# check_equality pgfexamples/template_parameter_synthesis/brp_obs_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/brp_obs_parameter_invariant.pgcl
 nat s;
 nat f;
 nat h;
diff --git a/pgfexamples/template_parameter_synthesis/dueling_cowboys_parameter.pgcl b/pgfexamples/template_parameter_synthesis/dueling_cowboys_parameter.pgcl
index 99212fc..5b5b9fa 100644
--- a/pgfexamples/template_parameter_synthesis/dueling_cowboys_parameter.pgcl
+++ b/pgfexamples/template_parameter_synthesis/dueling_cowboys_parameter.pgcl
@@ -1,3 +1,4 @@
+# check_equality pgfexamples/template_parameter_synthesis/dueling_cowboys_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/dueling_cowboys_parameter_invariant.pgcl
 nat t; // t = 0 player A's turn; t = 1 player B's turn; t>1 not interpretable
 nat c; // c=1, both player alive; c = 0 one player dead; c>1 not interpretable
 rparam a; // probability that Player A shoots player B in a turn.
diff --git a/pgfexamples/template_parameter_synthesis/geometric_observe_parameter.pgcl b/pgfexamples/template_parameter_synthesis/geometric_observe_parameter.pgcl
index cbe77b8..bec7251 100644
--- a/pgfexamples/template_parameter_synthesis/geometric_observe_parameter.pgcl
+++ b/pgfexamples/template_parameter_synthesis/geometric_observe_parameter.pgcl
@@ -1,3 +1,4 @@
+# check_equality pgfexamples/template_parameter_synthesis/geometric_observe_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/geometric_observe_parameter_invariant.pgcl
 nat y;
 nat x;
 nat tmp;
diff --git a/pgfexamples/template_parameter_synthesis/geometric_parameter.pgcl b/pgfexamples/template_parameter_synthesis/geometric_parameter.pgcl
index 92975a7..325430b 100644
--- a/pgfexamples/template_parameter_synthesis/geometric_parameter.pgcl
+++ b/pgfexamples/template_parameter_synthesis/geometric_parameter.pgcl
@@ -1,3 +1,4 @@
+# check_equality pgfexamples/template_parameter_synthesis/geometric_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/geometric_parameter_invariant.pgcl
 nat x;
 nat c;
 nat temp;
diff --git a/pgfexamples/template_parameter_synthesis/invariants/bit_flip_conditioning_generalized_parameter_invariant.pgcl b/pgfexamples/template_parameter_synthesis/invariants/bit_flip_conditioning_generalized_parameter_invariant.pgcl
index 8c8cb76..c0d0f94 100644
--- a/pgfexamples/template_parameter_synthesis/invariants/bit_flip_conditioning_generalized_parameter_invariant.pgcl
+++ b/pgfexamples/template_parameter_synthesis/invariants/bit_flip_conditioning_generalized_parameter_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 bool b1
 bool b2
 bool b3
diff --git a/pgfexamples/template_parameter_synthesis/invariants/bit_flip_conditioning_parameter_invariant.pgcl b/pgfexamples/template_parameter_synthesis/invariants/bit_flip_conditioning_parameter_invariant.pgcl
index 8832330..76af342 100644
--- a/pgfexamples/template_parameter_synthesis/invariants/bit_flip_conditioning_parameter_invariant.pgcl
+++ b/pgfexamples/template_parameter_synthesis/invariants/bit_flip_conditioning_parameter_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 bool b1
 bool b2
 bool b3
diff --git a/pgfexamples/template_parameter_synthesis/invariants/brp_obs_parameter_invariant.pgcl b/pgfexamples/template_parameter_synthesis/invariants/brp_obs_parameter_invariant.pgcl
index 46bb669..038f0fb 100644
--- a/pgfexamples/template_parameter_synthesis/invariants/brp_obs_parameter_invariant.pgcl
+++ b/pgfexamples/template_parameter_synthesis/invariants/brp_obs_parameter_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat s;
 nat f;
 nat h;
diff --git a/pgfexamples/template_parameter_synthesis/invariants/dueling_cowboys_parameter_invariant.pgcl b/pgfexamples/template_parameter_synthesis/invariants/dueling_cowboys_parameter_invariant.pgcl
index 257a4df..13e0fa1 100644
--- a/pgfexamples/template_parameter_synthesis/invariants/dueling_cowboys_parameter_invariant.pgcl
+++ b/pgfexamples/template_parameter_synthesis/invariants/dueling_cowboys_parameter_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat t; // t = 0 player A's turn; t = 1 player B's turn; t>1 not interpretable
 nat c; // c=1, both player alive; c = 0 one player dead; c>1 not interpretable
 rparam a; // probability that Player A shoots player B in a turn.
diff --git a/pgfexamples/template_parameter_synthesis/invariants/geometric_observe_parameter_invariant.pgcl b/pgfexamples/template_parameter_synthesis/invariants/geometric_observe_parameter_invariant.pgcl
index 209b2c7..108801b 100644
--- a/pgfexamples/template_parameter_synthesis/invariants/geometric_observe_parameter_invariant.pgcl
+++ b/pgfexamples/template_parameter_synthesis/invariants/geometric_observe_parameter_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat y;
 nat x;
 nat tmp;
diff --git a/pgfexamples/template_parameter_synthesis/invariants/geometric_parameter_invariant.pgcl b/pgfexamples/template_parameter_synthesis/invariants/geometric_parameter_invariant.pgcl
index b8f6a56..2111a46 100644
--- a/pgfexamples/template_parameter_synthesis/invariants/geometric_parameter_invariant.pgcl
+++ b/pgfexamples/template_parameter_synthesis/invariants/geometric_parameter_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat x;
 nat c;
 nat temp;
diff --git a/pgfexamples/template_parameter_synthesis/invariants/ky_die_parameter_invariant.pgcl b/pgfexamples/template_parameter_synthesis/invariants/ky_die_parameter_invariant.pgcl
index 6f3fff8..ca04c9a 100644
--- a/pgfexamples/template_parameter_synthesis/invariants/ky_die_parameter_invariant.pgcl
+++ b/pgfexamples/template_parameter_synthesis/invariants/ky_die_parameter_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat s;
 nat die;
 rparam p;
diff --git a/pgfexamples/template_parameter_synthesis/invariants/n_geometric_parameter_invariant.pgcl b/pgfexamples/template_parameter_synthesis/invariants/n_geometric_parameter_invariant.pgcl
index 782d9ac..61e3d2e 100644
--- a/pgfexamples/template_parameter_synthesis/invariants/n_geometric_parameter_invariant.pgcl
+++ b/pgfexamples/template_parameter_synthesis/invariants/n_geometric_parameter_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat n;
 nat c;
 nat tmp;
diff --git a/pgfexamples/template_parameter_synthesis/invariants/negative_binomial_parameter_invariant.pgcl b/pgfexamples/template_parameter_synthesis/invariants/negative_binomial_parameter_invariant.pgcl
index 2feed46..c4fad66 100644
--- a/pgfexamples/template_parameter_synthesis/invariants/negative_binomial_parameter_invariant.pgcl
+++ b/pgfexamples/template_parameter_synthesis/invariants/negative_binomial_parameter_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat n;
 nat i;
 nat temp;
diff --git a/pgfexamples/template_parameter_synthesis/invariants/negative_binomial_reversed_parameter_invariant.pgcl b/pgfexamples/template_parameter_synthesis/invariants/negative_binomial_reversed_parameter_invariant.pgcl
index 2feed46..c4fad66 100644
--- a/pgfexamples/template_parameter_synthesis/invariants/negative_binomial_reversed_parameter_invariant.pgcl
+++ b/pgfexamples/template_parameter_synthesis/invariants/negative_binomial_reversed_parameter_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat n;
 nat i;
 nat temp;
diff --git a/pgfexamples/template_parameter_synthesis/invariants/random_walk_parameter_invariant.pgcl b/pgfexamples/template_parameter_synthesis/invariants/random_walk_parameter_invariant.pgcl
index 3a5507f..0be24e5 100644
--- a/pgfexamples/template_parameter_synthesis/invariants/random_walk_parameter_invariant.pgcl
+++ b/pgfexamples/template_parameter_synthesis/invariants/random_walk_parameter_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat s;
 nat c;
 nat tmp;
diff --git a/pgfexamples/template_parameter_synthesis/ky_die_parameter.pgcl b/pgfexamples/template_parameter_synthesis/ky_die_parameter.pgcl
index b9e51c0..211f1a0 100644
--- a/pgfexamples/template_parameter_synthesis/ky_die_parameter.pgcl
+++ b/pgfexamples/template_parameter_synthesis/ky_die_parameter.pgcl
@@ -1,3 +1,4 @@
+# check_equality pgfexamples/template_parameter_synthesis/ky_die_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/ky_die_parameter_invariant.pgcl
 nat s;
 nat die;
 
diff --git a/pgfexamples/template_parameter_synthesis/n_geometric_parameter.pgcl b/pgfexamples/template_parameter_synthesis/n_geometric_parameter.pgcl
index e6a9f09..4084f51 100644
--- a/pgfexamples/template_parameter_synthesis/n_geometric_parameter.pgcl
+++ b/pgfexamples/template_parameter_synthesis/n_geometric_parameter.pgcl
@@ -1,3 +1,4 @@
+# check_equality pgfexamples/template_parameter_synthesis/n_geometric_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/n_geometric_parameter_invariant.pgcl
 nat n;
 nat c;
 nat tmp;
diff --git a/pgfexamples/template_parameter_synthesis/negative_binomial_parameter.pgcl b/pgfexamples/template_parameter_synthesis/negative_binomial_parameter.pgcl
index c8d1bce..e8d6546 100644
--- a/pgfexamples/template_parameter_synthesis/negative_binomial_parameter.pgcl
+++ b/pgfexamples/template_parameter_synthesis/negative_binomial_parameter.pgcl
@@ -1,3 +1,4 @@
+# check_equality pgfexamples/template_parameter_synthesis/negative_binomial_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/negative_binomial_parameter_invariant.pgcl
 nat n;
 nat i;
 nat temp;
diff --git a/pgfexamples/template_parameter_synthesis/negative_binomial_reversed_parameter.pgcl b/pgfexamples/template_parameter_synthesis/negative_binomial_reversed_parameter.pgcl
index e671bbd..a2eea38 100644
--- a/pgfexamples/template_parameter_synthesis/negative_binomial_reversed_parameter.pgcl
+++ b/pgfexamples/template_parameter_synthesis/negative_binomial_reversed_parameter.pgcl
@@ -1,3 +1,4 @@
+# check_equality pgfexamples/template_parameter_synthesis/negative_binomial_reversed_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/negative_binomial_reversed_parameter_invariant.pgcl
 nat n;
 nat i;
 nat temp;
diff --git a/pgfexamples/template_parameter_synthesis/random_walk_parameter.pgcl b/pgfexamples/template_parameter_synthesis/random_walk_parameter.pgcl
index e85acb9..e97a03d 100644
--- a/pgfexamples/template_parameter_synthesis/random_walk_parameter.pgcl
+++ b/pgfexamples/template_parameter_synthesis/random_walk_parameter.pgcl
@@ -1,3 +1,4 @@
+# check_equality pgfexamples/template_parameter_synthesis/random_walk_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/random_walk_parameter_invariant.pgcl
 nat s;
 nat c;
 nat tmp;
diff --git a/pgfexamples/template_parameter_synthesis/telephone_operator_parameter.pgcl b/pgfexamples/template_parameter_synthesis/telephone_operator_parameter.pgcl
index 6241038..8960833 100644
--- a/pgfexamples/template_parameter_synthesis/telephone_operator_parameter.pgcl
+++ b/pgfexamples/template_parameter_synthesis/telephone_operator_parameter.pgcl
@@ -1,3 +1,6 @@
+# skip
+# TODO this has no invariant file
+# check_equality pgfexamples/template_parameter_synthesis/telephone_operator_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/telephone_operator_parameter_invariant.pgcl
 nat x; // 0: weekday, 1: weekend
 nat d; // sample the number of phone calls received in one hour.
 rparam p;
diff --git a/prodigy/analysis/equivalence/equivalence_check.py b/prodigy/analysis/equivalence/equivalence_check.py
index 9c1adae..cf33a15 100644
--- a/prodigy/analysis/equivalence/equivalence_check.py
+++ b/prodigy/analysis/equivalence/equivalence_check.py
@@ -12,7 +12,6 @@
 from prodigy.analysis.instructionhandler.program_info import ProgramInfo
 from prodigy.analysis.solver.solver_type import SolverType
 from prodigy.distribution.distribution import Distribution, State
-from prodigy.pgcl.pgcl_operations import cav_phi
 from prodigy.util.color import Style
 from prodigy.util.logger import log_setup
 
@@ -50,7 +49,7 @@ def generate_equivalence_test_distribution(
 
 def check_equivalence(
         program: Program,
-        invariant: Program,
+        other_program: Program,
         config: ForwardAnalysisConfig,
         analyzer: Callable[
             [Union[Instr, Sequence[Instr]], ProgramInfo, Distribution, Distribution, ForwardAnalysisConfig],
@@ -68,62 +67,70 @@ def check_equivalence(
     the second order distributions generated by the invariant and the once unrolled while
     loop of the program. If this difference can be made equal to 0, the programs are
     equivalent.
-    .. param config: The configuration.
-    .. param program: The While-Loop program
-    .. param invariant: The loop-free invariant
-    .. returns: Whether the invariant and the program are equivalent.
+    :param config: The configuration.
+    :param program: The first program
+    :param other_program: The second program
+    :params analyzer: The analyzer.
+    :returns: Whether the invariant and the program are equivalent.
     """
 
     logger.debug("Checking equivalence.")
-    # First we create the modified input program in order to fit the premise of Park's Lemma
-    modified_inv = cav_phi(program, invariant)
+
+    # If both programs do not have the same variables, they are not equal
+    if set(program.variables.keys()).difference(set(other_program.variables.keys())) != set():
+        logger.info("The two programs already have different variable sets, prog: %s, other: %s",
+                    program.variables.keys(), other_program.variables.keys())
+        return False, State()   # TODO how should the state look like?
 
     # Now we have to generate an infinite state parametrized distribution for every program variable.
     test_dist, new_vars = generate_equivalence_test_distribution(program, config)
 
     # Compute the resulting distributions for both programs
-    logger.debug("Compute the modified invariant...")
-    modified_inv_result, modified_inv_error = analyzer(
-        modified_inv.instructions,
-        ProgramInfo(modified_inv, so_vars=frozenset(new_vars.keys())),
+    logger.debug("Compute the other programs posterior...")
+    other_program_posterior, other_program_error = analyzer(
+        other_program.instructions,
+        ProgramInfo(other_program, so_vars=frozenset(new_vars.keys())),
         test_dist,
-        config.factory.from_expr("0", *(modified_inv.variables | new_vars.keys())),
+        config.factory.from_expr("0", *(other_program.variables | new_vars.keys())),
         config
     )
-    logger.debug("modified invariant result:\n%s", modified_inv_result)
-    logger.debug("Compute the invariant...")
+    logger.debug("other programs result:\n%s", other_program_posterior)
+    logger.debug("Compute the posterior of the program...")
 
     if config.show_intermediate_steps:
-        print(f"\n{Style.YELLOW} Compute the result of the invariant. {Style.RESET}")
-    inv_result, inv_error = analyzer(
-        invariant.instructions,
-        ProgramInfo(invariant, so_vars=frozenset(new_vars.keys())), test_dist,
-        config.factory.one(*(modified_inv.variables | new_vars.keys())) * 0, config)
-    logger.debug("invariant result:\n%s", inv_result)
+        print(f"\n{Style.YELLOW} Compute the posterior of the program. {Style.RESET}")
+    program_posterior, program_error = analyzer(
+        program.instructions,
+        ProgramInfo(program, so_vars=frozenset(new_vars.keys())),
+        test_dist,
+        config.factory.one(*(program.variables | new_vars.keys())) * 0,
+        config
+    )
+    logger.debug("program result:\n%s", program_posterior)
 
-    diff = inv_result - modified_inv_result
+    diff = program_posterior - other_program_posterior
 
     # Compare them and check whether they are equal.
-    params = program.parameters.keys() | invariant.parameters.keys()
+    params = program.parameters.keys() | other_program.parameters.keys()
     solver = SolverType.make(config.solver_type)
-    dist_is_solution, dist_candidates = solver.solve(inv_result.set_parameters(*params),
-                                                     modified_inv_result.set_parameters(*params))
-    err_is_solution, err_candidates = solver.solve(inv_error.set_parameters(*params),
-                                                   modified_inv_error.set_parameters(*params))
+    dist_is_solution, dist_candidates = solver.solve(program_posterior.set_parameters(*params),
+                                                     other_program_posterior.set_parameters(*params))
+    err_is_solution, err_candidates = solver.solve(program_error.set_parameters(*params),
+                                                   other_program_error.set_parameters(*params))
 
     # If there is no solution tell the user why.
     if (dist_is_solution and err_is_solution) is False:
-        logger.debug("Invariant validation failed.")
+        logger.debug("Equivalence refuted.")
         state, _ = diff.get_state()
         return False, State({var: state[sym] for sym, var in new_vars.items()})
 
     # If there is a solution, individually, see whether they match.
     if (dist_is_solution and err_is_solution) is True:
         if not dist_candidates:
-            logger.debug("Invariant validated.")
+            logger.debug("Posterior equivalence validated.")
             return True, err_candidates
         if not err_candidates:
-            logger.debug("Invariant validated.")
+            logger.debug("Posterior error validated.")
             return True, dist_candidates
         logger.debug("Matching individual solutions\n%s\n%s", dist_candidates, err_candidates)
         res_both = []
@@ -138,5 +145,7 @@ def check_equivalence(
             logger.debug("Current partial solution space: %s", res_both)
             if len(res_both) == 0:
                 return False, State()  # TODO how to generate a counterexample here?
+        logger.debug("Equivalence validated.")
         return True, res_both
+    logger.debug("Equivalence unknown.")
     return None, diff
diff --git a/prodigy/analysis/evtinvariants/invariant_synthesis.py b/prodigy/analysis/evtinvariants/invariant_synthesis.py
index 50279ad..a439508 100644
--- a/prodigy/analysis/evtinvariants/invariant_synthesis.py
+++ b/prodigy/analysis/evtinvariants/invariant_synthesis.py
@@ -33,7 +33,6 @@ def evt_invariant_synthesis(loop: WhileInstr,
     # enumerate potential candidates given by a heuristic
     for evt_candidate in strategy.template_heuristics.generate():
         print(f"{Style.YELLOW}Invariant candidate: {evt_candidate}{Style.RESET}{Style.CLEARTOEND}", end="\r")
-
         # Compute one iteration step.
         evt_inv = evt_candidate
         one_step_dist, one_step_err = analyzer(loop.body, prog_info, evt_inv.filter(loop.cond), zero_dist, config)
@@ -45,13 +44,11 @@ def evt_invariant_synthesis(loop: WhileInstr,
             solver = SolverType.make(config.solver_type, config.factory)
         else:
             solver = SolverType.make(config.solver_type)
-
         # Check equality between the iterated expression and the invariant.
         logger.debug("Check Invariant candidate %s", evt_inv)
         is_solution, solution_candidates = solver.solve(evt_inv, phi_inv)
         if is_solution is False or is_solution is None:
             continue
-
         logger.debug("Filter solutions in: %s", solution_candidates)
 
         # Exclude "all zero" solutions, as well as solutions which make the denominator 0.
@@ -65,7 +62,9 @@ def evt_invariant_synthesis(loop: WhileInstr,
             # which make the denominator zero
             if denominator.subs(candidate).equals(0):
                 continue
-            solutions.append(candidate)
+
+            if candidate not in solutions:
+                solutions.append(candidate)
 
         # In case there are still some solutions we check them for actual solutions in the FPS domain with non-negative
         # coefficients. This is in general a hard problem (not known to be decidable), thus we use heuristics.
diff --git a/prodigy/analysis/instructionhandler/while_handler.py b/prodigy/analysis/instructionhandler/while_handler.py
index 5d932dc..e38f178 100644
--- a/prodigy/analysis/instructionhandler/while_handler.py
+++ b/prodigy/analysis/instructionhandler/while_handler.py
@@ -18,6 +18,7 @@
 from prodigy.analysis.instructionhandler.program_info import ProgramInfo
 from prodigy.distribution import Distribution, State
 from prodigy.distribution.generating_function import SympyPGF
+from prodigy.pgcl.pgcl_operations import cav_phi
 from prodigy.util.color import Style
 from prodigy.util.logger import print_progress_bar, log_setup
 
@@ -47,8 +48,12 @@ def _analyze_with_invariant(
                            instructions=[instruction],
                            functions=prog_info.functions)
             print(f"{Style.YELLOW}Verifying invariant...{Style.RESET}")
+
+            # First we create the modified input program in order to fit the premise of Park's Lemma
+            phi_inv = cav_phi(prog, inv_prog)
+
             answer, result = check_equivalence(
-                prog, inv_prog, config, analyzer)
+                inv_prog, phi_inv, config, analyzer)
             if answer:
                 assert isinstance(result, list)
                 if len(result) == 0:
@@ -204,7 +209,6 @@ def _evt_invariant(
                     solutions.append(candidate)
         if len(solutions) > 0:
             print(f"All solutions: {solutions}")
-            # TODO use a solution to compute the final distribution.
             logger.info("Using the first solution to continue.")
             sol_dist = config.factory.from_expr(
                 sympy.S(str(evt_inv - evt_inv.filter(instruction.cond))).subs(solutions[0]))
diff --git a/prodigy/analysis/solver/sympy_solver.py b/prodigy/analysis/solver/sympy_solver.py
index 1ae5baa..9274119 100644
--- a/prodigy/analysis/solver/sympy_solver.py
+++ b/prodigy/analysis/solver/sympy_solver.py
@@ -19,26 +19,33 @@ def solve(self, f: Distribution, g: Distribution) -> Tuple[Optional[bool], List[
         s_equation = sympy.sympify(str(f - g))
 
         if s_parameters:
-            solutions = sympy.solve_undetermined_coeffs(s_equation, s_parameters, *s_variables, dict=True,
-                                                        particular=True)
-            # validate solutions:
-
-            # no solutions or infinitely many found.
-            if not len(solutions) > 0:
-                if s_equation.equals(0):
-                    self.logger.debug("All parameter value combinations are valid.")
-                    return True, []
-                self.logger.debug("No solutions exist.")
-                return False, []
 
-            # at least one solution found
-            for sol in solutions:
-                for _, val in sol.items():
-                    if not val.free_symbols <= s_parameters:
-                        self.logger.info("SympySolver produced the invalid result %s.", sol)
-                        return None, []
-            self.logger.debug("solutions found: %s", solutions)
-            return True, solutions
+            try:
+                solutions = sympy.solve_undetermined_coeffs(s_equation, s_parameters, *s_variables,
+                                                            dict=True, particular=True)
+
+                # validate solutions:
+                # no solutions or infinitely many found.
+                if not len(solutions) > 0:
+                    if s_equation.equals(0):
+                        self.logger.debug("All parameter value combinations are valid.")
+                        return True, []
+                    self.logger.debug("No solutions exist.")
+                    return False, []
+
+                # at least one solution found
+                for sol in solutions:
+                    for _, val in sol.items():
+                        if not val.free_symbols <= s_parameters:
+                            self.logger.info("SympySolver produced the invalid result %s.", sol)
+                            return None, []
+                self.logger.debug("solutions found: %s", solutions)
+                return True, solutions
+
+            except NotImplementedError as e:
+                if "no valid subset found" in str(e):
+                    self.logger.info("No solution for %s", s_equation)
+                    return False, []
 
         else:
             is_equal = s_equation.equals(0)
diff --git a/prodigy/cli.py b/prodigy/cli.py
index 5a5b1f2..022c1d2 100644
--- a/prodigy/cli.py
+++ b/prodigy/cli.py
@@ -27,6 +27,7 @@
 from prodigy.analysis.exceptions import VerificationError
 from prodigy.analysis.instructionhandler.program_info import ProgramInfo
 from prodigy.analysis.solver.solver_type import SolverType
+from prodigy.analysis.independence.independence import independent_vars as independent_vars_analysis
 from prodigy.distribution.distribution import State
 from prodigy.util.color import Style
 from prodigy.util.logger import log_setup
@@ -125,8 +126,8 @@ def main(ctx, program_file: IO, input_dist: str,
 @cli.command('check_equality')
 @click.pass_context
 @click.argument('program_file', type=click.File('r'))
-@click.argument('invariant_file', type=click.File('r'))
-def check_equality(ctx, program_file: IO, invariant_file: IO):
+@click.argument('other_program_file', type=click.File('r'))
+def check_equality(ctx, program_file: IO, other_program_file: IO):
     """
     Checks whether a certain loop-free program is an invariant of a specified while loop.
     :param program_file: the file containing the while-loop
@@ -134,18 +135,18 @@ def check_equality(ctx, program_file: IO, invariant_file: IO):
     :return:
     """
     prog_src = program_file.read()
-    inv_src = invariant_file.read()
+    other_prog_src = other_program_file.read()
 
     prog = compiler.parse_pgcl(prog_src)
     if isinstance(prog, CheckFail):
         raise ValueError(f"Could not compile the Program. {prog}")
 
-    inv = compiler.parse_pgcl(inv_src)
-    if isinstance(inv, CheckFail):
-        raise ValueError(f"Could not compile invariant. {inv}")
+    other_prog = compiler.parse_pgcl(other_prog_src)
+    if isinstance(other_prog, CheckFail):
+        raise ValueError(f"Could not compile invariant. {other_prog}")
 
     start = time.perf_counter()
-    equiv, result = check_equivalence(prog, inv, ctx.obj['CONFIG'], compute_semantics)
+    equiv, result = check_equivalence(prog, other_prog, ctx.obj['CONFIG'], compute_semantics)
     stop = time.perf_counter()
     if equiv is True:
         assert isinstance(result, list)
@@ -193,7 +194,7 @@ def independent_vars(ctx, program_file: IO, compute_exact: bool):
         raise ValueError(f"Could not compile the Program. {prog}")
 
     start = time.perf_counter()
-    indep_rel: Set[frozenset[Var]] = independent_vars(prog, program_file, compute_exact)
+    indep_rel: Set[frozenset[Var]] = independent_vars_analysis(prog) #, program_file, compute_exact)
     stop = time.perf_counter()
     print(Style.OKBLUE + "Under-approximation: \t" + str(indep_rel) +
           Style.RESET)
diff --git a/prodigy/pgcl/pgcl_operations.py b/prodigy/pgcl/pgcl_operations.py
index 94503e3..a88dc97 100644
--- a/prodigy/pgcl/pgcl_operations.py
+++ b/prodigy/pgcl/pgcl_operations.py
@@ -16,8 +16,8 @@
 def make_else_if(instructions: List[Tuple[BinopExpr, List[Instr]]]) -> IfInstr:
     """Creates an else-if chain from a list of conditions and bodies for if-instructions"""
 
-    outer_instr: IfInstr = None
-    curr_instr: IfInstr = None
+    outer_instr: IfInstr | None = None
+    curr_instr: IfInstr | None = None
     for cond, body in instructions:
         instr = IfInstr(cond=cond, true=body, false=None)
         if outer_instr is None:
@@ -25,8 +25,8 @@ def make_else_if(instructions: List[Tuple[BinopExpr, List[Instr]]]) -> IfInstr:
         if curr_instr is not None:
             curr_instr.false = [instr]
         curr_instr = instr
-
-    curr_instr.false = [SkipInstr()]
+    if curr_instr:
+        curr_instr.false = [SkipInstr()]
     return outer_instr
 
 
diff --git a/pyproject.toml b/pyproject.toml
index 3234d23..0bbc04d 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -45,6 +45,7 @@ yapf = "^0.30.0"
 jinja2 = "3.1.4"
 rope = "^0.17.0"
 pytest-cov = "^2.9.0"
+pytest-ordering = "^0.6"
 hypothesis = "^5.18.0"
 
 [tool.poetry.scripts]
diff --git a/tests/analysis/equivalence/test_equivalence_check.py b/tests/analysis/equivalence/test_equivalence_check.py
index a842d19..136ae46 100644
--- a/tests/analysis/equivalence/test_equivalence_check.py
+++ b/tests/analysis/equivalence/test_equivalence_check.py
@@ -1,17 +1,24 @@
+import builtins
+import os
+from glob import glob
+from os.path import isfile
+
 import pytest
 import sympy
+from probably.pgcl import parse_pgcl
 from probably.pgcl.ast import Program
 from probably.pgcl.compiler import compile_pgcl
 
 from prodigy.analysis.analyzer import compute_semantics
 from prodigy.analysis.config import ForwardAnalysisConfig
 from prodigy.analysis.equivalence.equivalence_check import check_equivalence
+from prodigy.pgcl.pgcl_operations import cav_phi
 
 
 @pytest.mark.parametrize(
     'engine',
     [ForwardAnalysisConfig.Engine.GINAC, ForwardAnalysisConfig.Engine.SYMPY, ForwardAnalysisConfig.Engine.SYMENGINE])
-def test_equivalence_check(engine):
+def test_equivalence_check_geometric_sampler(engine):
     prog = compile_pgcl("""
         nat x;
         nat c;
@@ -37,7 +44,9 @@ def test_equivalence_check(engine):
         } else {skip}
     """)
     assert isinstance(inv, Program)
-    res, subs = check_equivalence(prog, inv, ForwardAnalysisConfig(engine=engine), compute_semantics)
+
+    phi_inv = cav_phi(prog, inv)
+    res, subs = check_equivalence(phi_inv, inv, ForwardAnalysisConfig(engine=engine), compute_semantics)
     assert res
     assert subs == []
 
@@ -73,7 +82,110 @@ def test_equivalence_check_parameter(engine):
         } else {skip}
     """)
     assert isinstance(inv, Program)
-    res, subs = check_equivalence(prog, inv, ForwardAnalysisConfig(engine=engine), compute_semantics)
+
+    phi_inv = cav_phi(prog, inv)
+    res, subs = check_equivalence(phi_inv, inv, ForwardAnalysisConfig(engine=engine), compute_semantics)
     assert res
     assert len(subs) == 1
     assert sympy.S(subs[0][sympy.S('p')]) == sympy.S('0.5') or sympy.S(subs[0][sympy.S('p')]) == sympy.S('1/2')
+
+
+@pytest.mark.parametrize(
+    "engine",
+    [ForwardAnalysisConfig.Engine.GINAC, ForwardAnalysisConfig.Engine.SYMPY,
+     ForwardAnalysisConfig.Engine.SYMENGINE]
+)
+@pytest.mark.parametrize(
+    "file_path",
+    [y for x in os.walk("pgfexamples/equivalence/loop_free") for y in glob(os.path.join(x[0], '*.pgcl')) if
+     not y.endswith('2.pgcl')]
+)
+def test_equivalence_loop_free_benchmarks(engine, file_path):
+    # Read the body of the program files
+    with open(file_path, "r") as f:
+        file = "\n".join(f.readlines())
+    file2_path = file_path.replace(".pgcl", "2.pgcl")
+    with open(file2_path, "r") as f:
+        inv = "\n".join(f.readlines())
+
+    # Compile them to a program object
+    prog1 = compile_pgcl(file)
+    prog2 = compile_pgcl(inv)
+
+    assert (isinstance(prog1, Program))
+    assert (isinstance(prog2, Program))
+
+    # Run the main program
+    res, subs = check_equivalence(prog1, prog2, ForwardAnalysisConfig(engine=engine), compute_semantics)
+    assert res
+    assert subs == []
+
+@pytest.mark.parametrize(
+    "engine",
+    [ ForwardAnalysisConfig.Engine.GINAC,ForwardAnalysisConfig.Engine.SYMPY,
+     # ForwardAnalysisConfig.Engine.SYMENGINE
+     ]
+)
+@pytest.mark.parametrize(
+    "file_path",
+    [y for x in os.walk("pgfexamples/equivalence/loopy") for y in glob(os.path.join(x[0], '*.pgcl')) if
+     not "invariants" in y]
+)
+# This test apparently has some side-effect which fails other tests (cf. #64), if it is executed last
+# this problem does not occur
+# FIXME this test has some effect on GINAC, when removing GINAC from the engine list, all tests pass
+def test_equivalence_loopy_benchmarks(monkeypatch, engine, file_path):
+    # Read the body of the program files
+    with open(file_path, "r") as f:
+        lines = f.readlines()
+        if "skip" in lines[0]:
+            pytest.skip("File marked as skipped")
+        file = "\n".join(lines)
+
+    invariant_path = file_path.replace("loopy/", "loopy/invariants/").replace(".pgcl", "_invariant.pgcl")
+    if not isfile(invariant_path):
+        pytest.skip("File has multiple invariants")
+
+    with open(invariant_path, "r") as f:
+        inv = "\n".join(f.readlines())
+
+    # Compile them to a program object
+    prog1 = parse_pgcl(file)
+    prog2 = parse_pgcl(inv)
+
+    assert (isinstance(prog1, Program))
+    assert (isinstance(prog2, Program))
+
+    inputs = iter(["1", invariant_path])
+    # Simulate the input for the invariant files
+    with monkeypatch.context() as m:
+        m.setattr("builtins.input", lambda _: next(inputs))  # Select invariant file1
+        # Run the main program
+        res, subs = check_equivalence(prog1, prog2, ForwardAnalysisConfig(engine=engine), compute_semantics)
+
+    assert res
+    assert subs == []
+
+
+@pytest.mark.parametrize(
+    "engine",
+    [ForwardAnalysisConfig.Engine.GINAC, ForwardAnalysisConfig.Engine.SYMPY,
+     # ForwardAnalysisConfig.Engine.SYMENGINE
+     ]
+)
+def test_equivalence_fail(engine):
+    prog1 = compile_pgcl("""
+    nat x;
+    x := geometric(1/2);
+    """)
+
+    prog2 = compile_pgcl("""
+    nat x;
+    x := unif(1,6);
+    """)
+
+    assert(isinstance(prog1, Program))
+    assert(isinstance(prog2, Program))
+
+    res, subs = check_equivalence(prog1, prog2, ForwardAnalysisConfig(engine=engine), compute_semantics)
+    assert not res
diff --git a/tests/analysis/handlers/test_sample_handler.py b/tests/analysis/handlers/test_sample_handler.py
index 5324a1d..e1ebe29 100644
--- a/tests/analysis/handlers/test_sample_handler.py
+++ b/tests/analysis/handlers/test_sample_handler.py
@@ -7,7 +7,6 @@
 from prodigy.distribution.generating_function import SympyPGF
 from prodigy.distribution.symengine_distribution import SymenginePGF
 
-
 @pytest.mark.parametrize('engine,factory',
                          [(ForwardAnalysisConfig.Engine.SYMPY, SympyPGF),
                           (ForwardAnalysisConfig.Engine.GINAC, ProdigyPGF),