diff --git a/.gitignore b/.gitignore
index 6a151e2b52..7fa1e2dabb 100644
--- a/.gitignore
+++ b/.gitignore
@@ -27,3 +27,4 @@ xcfa.c
 xcfa.dot
 xcfa.json
 *.plantuml
+xcfa-*.smt2
diff --git a/settings.gradle.kts b/settings.gradle.kts
index 91b45a0f0e..5abd19937b 100644
--- a/settings.gradle.kts
+++ b/settings.gradle.kts
@@ -39,6 +39,7 @@ include(
     "xcfa/c2xcfa",
     "xcfa/litmus2xcfa",
     "xcfa/llvm2xcfa",
+    "xcfa/xcfa2chc",
     "xcfa/xcfa-analysis",
     "xcfa/xcfa-cli",
 
diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprUtils.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprUtils.java
index 940719a148..bce86a7db8 100644
--- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprUtils.java
+++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprUtils.java
@@ -18,6 +18,7 @@
 import hu.bme.mit.theta.common.container.Containers;
 import hu.bme.mit.theta.core.decl.ConstDecl;
 import hu.bme.mit.theta.core.decl.Decl;
+import hu.bme.mit.theta.core.decl.IndexedConstDecl;
 import hu.bme.mit.theta.core.decl.ParamDecl;
 import hu.bme.mit.theta.core.decl.VarDecl;
 import hu.bme.mit.theta.core.model.ImmutableValuation;
@@ -27,6 +28,8 @@
 import hu.bme.mit.theta.core.type.anytype.RefExpr;
 import hu.bme.mit.theta.core.type.booltype.AndExpr;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
+import hu.bme.mit.theta.core.type.booltype.ExistsExpr;
+import hu.bme.mit.theta.core.type.booltype.ForallExpr;
 import hu.bme.mit.theta.core.type.booltype.NotExpr;
 import hu.bme.mit.theta.core.utils.IndexedVars.Builder;
 import hu.bme.mit.theta.core.utils.indexings.VarIndexing;
@@ -35,12 +38,15 @@
 import java.util.Collection;
 import java.util.Collections;
 import java.util.HashSet;
+import java.util.LinkedHashSet;
 import java.util.List;
 import java.util.Map;
+import java.util.Map.Entry;
 import java.util.Set;
 import java.util.stream.Collectors;
 
 import static com.google.common.base.Preconditions.checkNotNull;
+import static hu.bme.mit.theta.core.utils.TypeUtils.cast;
 
 /**
  * Utility functions related to expressions.
@@ -112,6 +118,69 @@ public static Collection<Expr<BoolType>> getConjuncts(final Expr<BoolType> expr)
         }
     }
 
+    /**
+     * Collect params of an expression into a given collection.
+     *
+     * @param expr      Expression
+     * @param collectTo Collection where the params should be put
+     */
+    public static void collectParams(final Expr<?> expr, final Collection<ParamDecl<?>> collectTo) {
+        if (expr instanceof RefExpr<?> refExpr) {
+            final Decl<?> decl = refExpr.getDecl();
+            if (decl instanceof ParamDecl<?> param) {
+                collectTo.add(param);
+                return;
+            }
+        }
+
+        if (expr instanceof ForallExpr forall) {
+            Set<ParamDecl<?>> params = new LinkedHashSet<>(getParams(forall.getOp()));
+            forall.getParamDecls().forEach(params::remove);
+            collectTo.addAll(params);
+        } else if (expr instanceof ExistsExpr exists) {
+            Set<ParamDecl<?>> params = new LinkedHashSet<>(getParams(exists.getOp()));
+            exists.getParamDecls().forEach(params::remove);
+            collectTo.addAll(params);
+        } else {
+            expr.getOps().forEach(op -> collectParams(op, collectTo));
+        }
+    }
+
+    /**
+     * Collect params from expressions into a given collection.
+     *
+     * @param exprs     Expressions
+     * @param collectTo Collection where the variables should be put
+     */
+    public static void collectParams(final Iterable<? extends Expr<?>> exprs, final Collection<ParamDecl<?>> collectTo) {
+        exprs.forEach(e -> collectParams(e, collectTo));
+    }
+
+    /**
+     * Get variables of an expression.
+     *
+     * @param expr Expression
+     * @return Set of variables appearing in the expression
+     */
+    public static Set<ParamDecl<?>> getParams(final Expr<?> expr) {
+        final Set<ParamDecl<?>> vars = Containers.createSet();
+        collectParams(expr, vars);
+        return vars;
+    }
+
+    /**
+     * Get variables of expressions.
+     *
+     * @param exprs Expressions
+     * @return Set of variables appearing in the expressions
+     */
+    public static Set<ParamDecl<?>> getParams(final Iterable<? extends Expr<?>> exprs) {
+        final Set<ParamDecl<?>> vars = Containers.createSet();
+        collectParams(exprs, vars);
+        return vars;
+    }
+
+
     /**
      * Collect variables of an expression into a given collection.
      *
@@ -165,6 +234,59 @@ public static Set<VarDecl<?>> getVars(final Iterable<? extends Expr<?>> exprs) {
         return vars;
     }
 
+    /**
+     * Collect indexed constants of an expression into a given collection.
+     *
+     * @param expr      Expression
+     * @param collectTo Collection where the constants should be put
+     */
+    public static void collectIndexedConstants(final Expr<?> expr, final Collection<IndexedConstDecl<?>> collectTo) {
+        if (expr instanceof RefExpr) {
+            final RefExpr<?> refExpr = (RefExpr<?>) expr;
+            final Decl<?> decl = refExpr.getDecl();
+            if (decl instanceof IndexedConstDecl<?>) {
+                final IndexedConstDecl<?> constDecl = (IndexedConstDecl<?>) decl;
+                collectTo.add(constDecl);
+                return;
+            }
+        }
+        expr.getOps().forEach(op -> collectIndexedConstants(op, collectTo));
+    }
+
+    /**
+     * Collect indexed constants from expressions into a given collection.
+     *
+     * @param exprs     Expressions
+     * @param collectTo Collection where the constants should be put
+     */
+    public static void collectIndexedConstants(final Iterable<? extends Expr<?>> exprs, final Collection<IndexedConstDecl<?>> collectTo) {
+        exprs.forEach(e -> collectIndexedConstants(e, collectTo));
+    }
+
+    /**
+     * Get indexed constants of an expression.
+     *
+     * @param expr Expression
+     * @return Set of constants appearing in the expression
+     */
+    public static Set<IndexedConstDecl<?>> getIndexedConstants(final Expr<?> expr) {
+        final Set<IndexedConstDecl<?>> consts = new HashSet<>();
+        collectIndexedConstants(expr, consts);
+        return consts;
+    }
+
+    /**
+     * Get indexed constants of expressions.
+     *
+     * @param exprs Expressions
+     * @return Set of constants appearing in the expressions
+     */
+    public static Set<IndexedConstDecl<?>> getIndexedConstants(final Iterable<? extends Expr<?>> exprs) {
+        final Set<IndexedConstDecl<?>> consts = new HashSet<>();
+        collectIndexedConstants(exprs, consts);
+        return consts;
+    }
+
     /**
      * Collect constants of an expression into a given collection.
      *
@@ -363,4 +485,22 @@ public static int nodeCountSize(final Expr<?> expr) {
         return 1 + expr.getOps().stream().map(ExprUtils::nodeCountSize).reduce(0, (x, y) -> x + y);
     }
 
+    /**
+     * Change fixed subexpressions using a lookup
+     *
+     * @param expr   the expr to change subexpressions in
+     * @param lookup the lookup mapping subexpression to replacements
+     * @return the changed expression
+     */
+    public static <T extends Type> Expr<T> changeSubexpr(Expr<T> expr, Map<Expr<?>, Expr<?>> lookup) {
+        if (lookup.containsKey(expr)) {
+            return cast(lookup.get(expr), expr.getType());
+        } else {
+            return expr.map(e -> changeSubexpr(e, lookup));
+        }
+    }
+
+    public static <T extends Type> Expr<T> changeDecls(Expr<T> expr, Map<? extends Decl<?>, ? extends Decl<?>> lookup) {
+        return changeSubexpr(expr, lookup.entrySet().stream().map(entry -> Map.entry(entry.getKey().getRef(), entry.getValue().getRef())).collect(Collectors.toMap(Entry::getKey, Entry::getValue)));
+    }
 }
diff --git a/subprojects/xcfa/xcfa-cli/build.gradle.kts b/subprojects/xcfa/xcfa-cli/build.gradle.kts
index 5e1c150d4c..dc92ba6f04 100644
--- a/subprojects/xcfa/xcfa-cli/build.gradle.kts
+++ b/subprojects/xcfa/xcfa-cli/build.gradle.kts
@@ -28,6 +28,7 @@ dependencies {
     implementation(project(":theta-analysis"))
     implementation(project(":theta-xcfa"))
     implementation(project(":theta-xcfa-analysis"))
+    implementation(project(":theta-xcfa2chc"))
     implementation(project(":theta-c2xcfa"))
     implementation(project(":theta-solver-z3"))
     implementation(project(":theta-solver-z3-legacy"))
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt
index 46ad6180f8..61794654c7 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt
@@ -59,6 +59,7 @@ import hu.bme.mit.theta.xcfa.passes.LbePass
 import hu.bme.mit.theta.xcfa.passes.LoopUnrollPass
 import hu.bme.mit.theta.xcfa.passes.StaticCoiPass
 import hu.bme.mit.theta.xcfa.toC
+import hu.bme.mit.theta.xcfa2chc.toSMT2CHC
 import java.io.File
 import java.util.concurrent.TimeUnit
 import kotlin.random.Random
@@ -245,6 +246,13 @@ private fun preVerificationLogging(
                 "Writing pre-verification artifacts to directory ${resultFolder.absolutePath}\n"
             )
 
+            if (!config.outputConfig.chcOutputConfig.disable) {
+                xcfa.procedures.forEach {
+                    val chcFile = File(resultFolder, "xcfa-${it.name}.smt2")
+                    chcFile.writeText(it.toSMT2CHC())
+                }
+            }
+
             if (!config.outputConfig.xcfaOutputConfig.disable) {
                 val xcfaDotFile = File(resultFolder, "xcfa.dot")
                 xcfaDotFile.writeText(xcfa.toDot())
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt
index ff6d663986..5c5af6f576 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt
@@ -330,6 +330,7 @@ data class OutputConfig(
 
     val cOutputConfig: COutputConfig = COutputConfig(),
     val xcfaOutputConfig: XcfaOutputConfig = XcfaOutputConfig(),
+    val chcOutputConfig: ChcOutputConfig = ChcOutputConfig(),
     val witnessConfig: WitnessConfig = WitnessConfig(),
     val argConfig: ArgConfig = ArgConfig(),
 ) : Config {
@@ -347,6 +348,11 @@ data class XcfaOutputConfig(
     var disable: Boolean = false,
 ) : Config
 
+data class ChcOutputConfig(
+    @Parameter(names = ["--disable-chc-serialization"])
+    var disable: Boolean = false,
+) : Config
+
 data class COutputConfig(
     @Parameter(names = ["--disable-c-serialization"])
     var disable: Boolean = false,
diff --git a/subprojects/xcfa/xcfa2chc/build.gradle.kts b/subprojects/xcfa/xcfa2chc/build.gradle.kts
new file mode 100644
index 0000000000..6bd82ed776
--- /dev/null
+++ b/subprojects/xcfa/xcfa2chc/build.gradle.kts
@@ -0,0 +1,25 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+plugins {
+    id("kotlin-common")
+}
+
+dependencies {
+    implementation(project(":theta-common"))
+    implementation(project(":theta-core"))
+    implementation(project(":theta-xcfa"))
+    implementation(project(":theta-solver-smtlib"))
+}
diff --git a/subprojects/xcfa/xcfa2chc/src/main/java/hu/bme/mit/theta/xcfa2chc/ChcUtils.kt b/subprojects/xcfa/xcfa2chc/src/main/java/hu/bme/mit/theta/xcfa2chc/ChcUtils.kt
new file mode 100644
index 0000000000..60d0a1c5ff
--- /dev/null
+++ b/subprojects/xcfa/xcfa2chc/src/main/java/hu/bme/mit/theta/xcfa2chc/ChcUtils.kt
@@ -0,0 +1,122 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
+package hu.bme.mit.theta.xcfa2chc
+
+import com.google.common.base.Preconditions.checkArgument
+import hu.bme.mit.theta.core.decl.Decls.Const
+import hu.bme.mit.theta.core.decl.Decls.Param
+import hu.bme.mit.theta.core.decl.ParamDecl
+import hu.bme.mit.theta.core.type.Expr
+import hu.bme.mit.theta.core.type.Type
+import hu.bme.mit.theta.core.type.booltype.BoolExprs.*
+import hu.bme.mit.theta.core.type.booltype.BoolType
+import hu.bme.mit.theta.core.type.functype.FuncExprs
+import hu.bme.mit.theta.core.type.functype.FuncType
+import hu.bme.mit.theta.core.utils.ExprUtils
+import hu.bme.mit.theta.solver.smtlib.impl.generic.GenericSmtLibSymbolTable
+import hu.bme.mit.theta.solver.smtlib.impl.generic.GenericSmtLibTransformationManager
+import java.util.*
+
+/*
+We want to be able to write logical derivations in the following way:
+
+head_name(vars) +=  // derivations
+    expr(vars).
+
+head_name(grounds) // facts
+
+!head_name(vars) with exprs(vars)  // queries
+ */
+
+open class Relation(val name: String, vararg paramTypes: Type) {
+    companion object {
+        private fun funcType(params: List<Type>, finalType: Type): FuncType<*, *> {
+            return if(params.size == 1) {
+                FuncType.of(params[0], finalType)
+            } else if(params.size > 1) {
+                FuncType.of(params[0], funcType(params.subList(1, params.size), finalType))
+            } else {
+                error("Nullary functions aren't handled here.")
+            }
+        }
+    }
+    val arity: Int = paramTypes.size
+    val rules: MutableList<Rule> = LinkedList()
+    val constDecl = if(arity == 0) Const(name, Bool()) else Const(name, funcType(paramTypes.toList(), Bool()))
+    open operator fun invoke(params: List<Expr<*>>) = RelationApp(this, params)
+    open operator fun invoke(vararg params: Expr<*>) = RelationApp(this, params.toList())
+}
+
+data class RelationApp(val relation: Relation, val params: List<Expr<*>>, val constraints: List<Expr<BoolType>> = emptyList()) {
+    init {
+        checkArgument(params.size == relation.arity)
+    }
+    val expr: Expr<BoolType> by lazy {
+        val coreExpr = if(params.size >= 1) {
+            FuncExprs.App(relation.constDecl.ref as Expr<FuncType<in Type, BoolType>>, params.map { it })
+        } else {
+            relation.constDecl.ref as Expr<BoolType>
+        }
+        if(constraints.isEmpty()) {
+            coreExpr
+        } else {
+            And(constraints + coreExpr)
+        }
+    }
+
+    operator fun plusAssign(constraints: List<Expr<BoolType>>) { relation.rules.add(Rule(expr, constraints)) }
+    operator fun plusAssign(constraint: Expr<BoolType>) { relation.rules.add(Rule(expr, listOf(constraint))) }
+
+    operator fun not() { relation.rules.add(Rule(False(), listOf(expr))) }
+    operator fun unaryPlus() { relation.rules.add(Rule(expr, listOf())) }
+    infix fun with(constraints: List<Expr<BoolType>>) = copy(constraints = this.constraints + constraints)
+    infix fun with(constraint: Expr<BoolType>) = copy(constraints = this.constraints + constraint)
+}
+data class Rule(val head: Expr<BoolType>, val constraints: List<Expr<BoolType>>) {
+    fun toExpr() = Forall(ExprUtils.getParams(head) + ExprUtils.getParams(constraints), Imply(And(constraints), head))
+}
+
+operator fun Expr<BoolType>.plus(other: Expr<BoolType>) = listOf(this, other)
+
+data class ParamHolder<T: Type>(private val type: T) {
+    private val lookup = LinkedHashMap<Int, ParamDecl<T>>()
+    operator fun get(i: Int) = lookup.getOrPut(i) { Param("P$i", type) }.ref
+}
+
+fun List<Relation>.toSMT2(): String {
+    val symbolTable = GenericSmtLibSymbolTable()
+    val transformationManager = GenericSmtLibTransformationManager(symbolTable)
+    val terms = flatMap { it.rules.map {  "(assert " + transformationManager.toTerm(it.toExpr()) + ")" } }
+    val decls = map { symbolTable.getDeclaration(it.constDecl) }
+
+    return """
+; generated by Theta
+; https://github.com/ftsrg/theta/
+
+(set-logic HORN)
+
+; declarations
+${decls.joinToString("\n")}
+
+; facts, rules, queries
+${terms.joinToString("\n")}
+
+(check-sat)
+(exit)
+""".trimIndent()
+}
+fun Relation.toSMT2() = listOf(this).toSMT2()
diff --git a/subprojects/xcfa/xcfa2chc/src/main/java/hu/bme/mit/theta/xcfa2chc/Xcfa2Chc.kt b/subprojects/xcfa/xcfa2chc/src/main/java/hu/bme/mit/theta/xcfa2chc/Xcfa2Chc.kt
new file mode 100644
index 0000000000..8c3849de4d
--- /dev/null
+++ b/subprojects/xcfa/xcfa2chc/src/main/java/hu/bme/mit/theta/xcfa2chc/Xcfa2Chc.kt
@@ -0,0 +1,71 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
+package hu.bme.mit.theta.xcfa2chc
+
+import hu.bme.mit.theta.core.decl.Decls.Param
+import hu.bme.mit.theta.core.type.arraytype.ArrayType
+import hu.bme.mit.theta.core.type.booltype.BoolExprs.And
+import hu.bme.mit.theta.core.type.booltype.BoolExprs.True
+import hu.bme.mit.theta.core.type.inttype.IntExprs.Int
+import hu.bme.mit.theta.core.utils.ExprUtils
+import hu.bme.mit.theta.core.utils.PathUtils
+import hu.bme.mit.theta.core.utils.StmtUtils
+import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory
+import hu.bme.mit.theta.xcfa.collectVars
+import hu.bme.mit.theta.xcfa.model.XcfaProcedure
+
+fun XcfaProcedure.toCHC(): List<Relation> {
+    val i2i = ArrayType.of(Int(), Int())
+
+    val vars = edges.flatMap { it.label.collectVars() }.toSet().toList()
+
+    val types = vars.map { it.type }.toTypedArray()
+    val oldParams = vars.associateWith { Param("|" + it.name + "|", it.type) }
+    val oldParamList = vars.map { oldParams[it]!!.ref }.toTypedArray()
+    val newParams = vars.associateWith { Param("|" + it.name + "_new|", it.type) }
+
+    val ufs = locs.associateWith { Relation(it.name, *types) } // br, co, rf, com
+
+    edges.forEach {
+        val unfoldResult = StmtUtils.toExpr(it.label.toStmt(), VarIndexingFactory.basicVarIndexing(0))
+        val expr = PathUtils.unfold(And(unfoldResult.exprs), VarIndexingFactory.indexing(0))
+        // var[0] is oldParam, var[-1]is newParam, everything else is a fresh param
+        var cnt = 0
+        val consts = ExprUtils.getIndexedConstants(expr).associateWith {
+            if(it.index == 0) oldParams[it.varDecl]!!
+            else if (it.index == unfoldResult.indexing[it.varDecl]) newParams[it.varDecl]!!
+            else Param("__tmp_${cnt++}", it.type)
+        }
+        val newParamList = vars.map { if(unfoldResult.indexing[it] == 0) oldParams[it]!!.ref else newParams[it]!!.ref }.toTypedArray()
+        val paramdExpr = ExprUtils.changeDecls(expr, consts)
+        (ufs[it.target]!!)(*newParamList) += (ufs[it.source]!!)(*oldParamList).expr + paramdExpr
+    }
+
+    if(errorLoc.isPresent) {
+        !(ufs[errorLoc.get()]!!(*oldParamList))
+    }
+
+    ufs[initLoc]!!(*oldParamList) += True()
+
+    return ufs.values.toList()
+}
+
+fun XcfaProcedure.toSMT2CHC(): String {
+    val chc = toCHC()
+    val smt2 = chc.toSMT2()
+    return smt2
+}
diff --git a/subprojects/xcfa/xcfa2chc/src/test/java/hu/bme/mit/theta/xcfa2chc/TestChcUtils.kt b/subprojects/xcfa/xcfa2chc/src/test/java/hu/bme/mit/theta/xcfa2chc/TestChcUtils.kt
new file mode 100644
index 0000000000..2e9f99aade
--- /dev/null
+++ b/subprojects/xcfa/xcfa2chc/src/test/java/hu/bme/mit/theta/xcfa2chc/TestChcUtils.kt
@@ -0,0 +1,537 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
+package hu.bme.mit.theta.xcfa2chc
+
+import hu.bme.mit.theta.core.decl.Decls
+import hu.bme.mit.theta.core.decl.ParamDecl
+import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.*
+import hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Read
+import hu.bme.mit.theta.core.type.arraytype.ArrayType
+import hu.bme.mit.theta.core.type.booltype.BoolExprs.*
+import hu.bme.mit.theta.core.type.inttype.IntExprs
+import hu.bme.mit.theta.core.type.inttype.IntExprs.Int
+import hu.bme.mit.theta.core.type.inttype.IntType
+import org.junit.jupiter.api.Test
+
+private val iParamLut = LinkedHashMap<String, ParamDecl<IntType>>()
+private fun iP(name: String) = iParamLut.getOrPut(name) { Decls.Param(name, IntExprs.Int()) }
+
+
+class TestChcUtils {
+
+    @Test
+    fun testPetersonManualCounting() {
+        val i2i = ArrayType.of(Int(), Int())
+
+        val pI = ParamHolder(Int())
+        val pA = ParamHolder(i2i)
+        val br = pA[9]
+        val po = pA[10]
+        val co = pA[11]
+        val rf = pA[12]
+        val com = pA[13]
+        val prevW = pI[14]
+        val eid = pI[15]
+        val eid2 = pI[17]
+        val vid = pI[18]
+        val vid3 = pI[19]
+        val eid3 = pI[20]
+        val eid4 = pI[21]
+        val eid5 = pI[22]
+        val eid6 = pI[23]
+        val vid4 = pI[24]
+        val eid7 = pI[25]
+        val eid8 = pI[26]
+        val vid5 = pI[27]
+        val eid9 = pI[28]
+        val eid10 = pI[29]
+        val eid11 = pI[50]
+
+        val turn = pI[30]
+        val flag1 = pI[31]
+        val flag2 = pI[32]
+        val cnt = pI[33]
+        val turn_old = pI[40]
+        val flag1_old = pI[41]
+        val flag2_old = pI[42]
+        val cnt_old = pI[43]
+
+        val init = Relation("init", i2i, i2i, i2i, i2i, Int()) // br, co, rf, com
+
+        val T0 = Relation("T0", i2i, i2i, i2i, i2i, Int(), Int(), Int(), Int(), Int()) // br, co, rf, com, eid, turn, flag0, flag1, cnt
+        val T0G = Relation("T0_gate", i2i, i2i, i2i, i2i, Int(), Int(), Int(), Int(), Int()) // br, co, rf, com, eid, turn, flag0, flag1, cnt
+        val T0C = Relation("T0_critical", i2i, i2i, i2i, i2i, Int(), Int(), Int(), Int(), Int()) // br, co, rf, com, eid, turn, flag0, flag1, cnt
+        val T0CF = Relation("T0_critical_final", i2i, i2i, i2i, i2i, Int(), Int(), Int(), Int(), Int()) // br, co, rf, com, eid, turn, flag0, flag1, cnt
+        val T0F = Relation("T0_final", i2i, i2i, i2i, i2i, Int(), Int(), Int(), Int(), Int()) // br, co, rf, com, eid, turn, flag0, flag1, cnt
+
+        val T1 = Relation("T1", i2i, i2i, i2i, i2i, Int(), Int(), Int(), Int(), Int()) // br, co, rf, com, eid, turn, flag0, flag1, cnt
+        val T1G = Relation("T1_gate", i2i, i2i, i2i, i2i, Int(), Int(), Int(), Int(), Int()) // br, co, rf, com, eid, turn, flag0, flag1, cnt
+        val T1C = Relation("T1_critical", i2i, i2i, i2i, i2i, Int(), Int(), Int(), Int(), Int()) // br, co, rf, com, eid, turn, flag0, flag1, cnt
+        val T1CF = Relation("T1_critical_final", i2i, i2i, i2i, i2i, Int(), Int(), Int(), Int(), Int()) // br, co, rf, com, eid, turn, flag0, flag1, cnt
+        val T1F = Relation("T1_final", i2i, i2i, i2i, i2i, Int(), Int(), Int(), Int(), Int()) // br, co, rf, com, eid, turn, flag0, flag1, cnt
+
+        val W = Relation("W", i2i, i2i, i2i, i2i, Int(), Int(), Int()) // br, co, rf, com, eid, vid, val
+
+        // problem: unique rf values (W->R) will disable some possible reads
+
+        init(br, co, rf, com, eid) +=
+            Eq(eid, Int(0)) +
+            Eq(Read(co, Int(0)), Int(0)) +
+            Eq(Read(com, Int(0)), Int(0))
+
+        W(br, co, rf, com, eid, vid, pI[0]) += // turn := 0
+            init(br, co, rf, com, eid).expr +
+                Eq(vid, Int(0)) +
+                Eq(pI[0], Int(0))
+        W(br, co, rf, com, eid, vid, pI[0]) += // flag0 := 0
+            init(br, co, rf, com, eid).expr +
+                Eq(vid, Int(1)) +
+                Eq(pI[0], Int(0))
+        W(br, co, rf, com, eid, vid, pI[0]) += // flag1 := 0
+            init(br, co, rf, com, eid).expr +
+                Eq(vid, Int(2)) +
+                Eq(pI[0], Int(0))
+        W(br, co, rf, com, eid, vid, pI[0]) += // cnt := 0
+            init(br, co, rf, com, eid).expr +
+                Eq(vid, Int(3)) +
+                Eq(pI[0], Int(0))
+
+        T0(br, co, rf, com, eid, turn, flag1, flag2, cnt) +=
+            init(br, co, rf, com, eid2).expr + Eq(eid, Int(1))
+        T1(br, co, rf, com, eid, turn, flag1, flag2, cnt) +=
+            init(br, co, rf, com, eid2).expr + Eq(eid, Int(2))
+
+        W(br, co, rf, com, eid, vid, pI[0]) += // flag0 := 1
+            W(br, co, rf, com, eid2, vid, pI[1]).expr + // prevW
+            T0(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr +
+                Eq(vid, Int(1)) +
+                Eq(pI[0], Int(1)) +
+                Eq(Add(Read(co, eid2), Int(1)), Read(co, eid)) + // co-next
+                Lt(Read(com, eid2), Read(com, eid))
+        W(br, co, rf, com, eid, vid, pI[0]) += // flag1 := 1
+            W(br, co, rf, com, eid2, vid, pI[1]).expr + // prevW
+            T1(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr +
+                Eq(vid, Int(2)) +
+                Eq(pI[0], Int(1)) +
+                Eq(Add(Read(co, eid2), Int(1)), Read(co, eid)) + // co-next
+                Lt(Read(com, eid2), Read(com, eid))
+
+        T0G(br, co, rf, com, eid2, turn, flag1, flag2, cnt) +=
+            W(br, co, rf, com, eid, vid, pI[0]).expr + // successful write
+            T0(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr + // previous loc
+                Eq(Add(eid, Int(2)), eid2) +               // eid update
+                Lt(Read(com, eid), Read(com, eid2))    // com constraint (because po)
+        T1G(br, co, rf, com, eid2, turn, flag1, flag2, cnt) +=
+            W(br, co, rf, com, eid, vid, pI[0]).expr + // successful write
+                T1(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr + // previous loc
+                Eq(Add(eid, Int(2)), eid2) +               // eid update
+                Lt(Read(com, eid), Read(com, eid2))    // com constraint (because po)
+
+        W(br, co, rf, com, eid, vid, pI[0]) += // turn := 0
+            W(br, co, rf, com, eid2, vid, pI[1]).expr + // prevW
+                T0G(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr +
+                Eq(vid, Int(0)) +
+                Eq(pI[0], Int(0)) +
+                Eq(Add(Read(co, eid2), Int(1)), Read(co, eid)) + // co-next
+                Lt(Read(com, eid2), Read(com, eid))
+        W(br, co, rf, com, eid, vid, pI[0]) += // turn := 1
+            W(br, co, rf, com, eid2, vid, pI[1]).expr + // prevW
+                T1G(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr +
+                Eq(vid, Int(0)) +
+                Eq(pI[0], Int(1)) +
+                Eq(Add(Read(co, eid2), Int(1)), Read(co, eid)) + // co-next
+                Lt(Read(com, eid2), Read(com, eid))
+
+        T0C(br, co, rf, com, eid2, turn, flag1, flag2, cnt) +=
+            W(br, co, rf, com, eid3, vid3, pI[1]).expr + // rf-source
+            W(br, co, rf, com, eid4, vid3, pI[2]).expr + // rf-source
+                Eq(Add(eid, Int(2)), eid9) +               // eid update
+                Eq(vid3, Int(2)) + // flag[1] read
+                Eq(Read(rf, eid3), eid9) + // rf
+                Lt(Read(com, eid3), Read(com, eid9)) +    // com constraint (because rf)
+                Lt(Read(com, eid9), Read(com, eid4)) +    // com constraint (because fr)
+                Eq(Add(Read(co, eid3), Int(1)), Read(co, eid4)) + // co-after is eid4
+                Eq(pI[1], flag2) +
+            W(br, co, rf, com, eid5, vid4, pI[2]).expr + // turn
+            W(br, co, rf, com, eid6, vid4, pI[3]).expr + // turn
+                Eq(Add(eid, Int(4)), eid10) +               // eid update
+                Eq(vid4, Int(0)) + // turn read
+                Eq(Read(rf, eid10), eid5)  + // rf
+                Lt(Read(com, eid5), Read(com, eid10)) +    // com constraint (because rf)
+                Lt(Read(com, eid10), Read(com, eid6)) +    // com constraint (because fr)
+                Eq(Add(Read(co, eid5), Int(1)), Read(co, eid6)) + // co-after is eid6
+                Eq(pI[2], turn) +
+            Or(Eq(turn, Int(0)), Eq(flag2, Int(0))) +
+            W(br, co, rf, com, eid7, vid5, pI[3]).expr + // turn
+            W(br, co, rf, com, eid8, vid5, pI[4]).expr + // turn
+                Eq(Add(eid, Int(6)), eid11) +               // eid update
+                Eq(vid5, Int(3)) + // turn read
+                Eq(Read(rf, eid11), eid7)  + // rf
+                Lt(Read(com, eid7), Read(com, eid11)) +    // com constraint (because rf)
+                Lt(Read(com, eid11), Read(com, eid8)) +    // com constraint (because fr)
+                Eq(Add(Read(co, eid7), Int(1)), Read(co, eid8)) + // co-after is eid8
+                Eq(pI[3], cnt) +
+            W(br, co, rf, com, eid, vid, pI[0]).expr + // successful write
+                T0G(br, co, rf, com, eid, turn_old, flag1, flag2_old, cnt_old).expr + // previous loc
+                Eq(Add(eid, Int(8)), eid2) +               // eid update
+                Lt(Read(com, eid), Read(com, eid9)) +      // com constraint (because po)
+                Lt(Read(com, eid9), Read(com, eid10)) +    // com constraint (because po)
+                Lt(Read(com, eid10), Read(com, eid11))  +   // com constraint (because po)
+                Lt(Read(com, eid11), Read(com, eid2))    // com constraint (because po)
+
+        T1C(br, co, rf, com, eid2, turn, flag1, flag2, cnt) +=
+            W(br, co, rf, com, eid3, vid3, pI[1]).expr + // rf-source
+            W(br, co, rf, com, eid4, vid3, pI[2]).expr + // rf-source
+                Eq(Add(eid, Int(2)), eid9) +               // eid update
+                Eq(vid3, Int(1)) + // flag[0] read
+                Eq(Read(rf, eid9), eid3) + // rf
+                Lt(Read(com, eid3), Read(com, eid9)) +    // com constraint (because rf)
+                Lt(Read(com, eid9), Read(com, eid4)) +    // com constraint (because fr)
+                Eq(Add(Read(co, eid3), Int(1)), Read(co, eid4)) + // co-after is eid4
+                Eq(pI[1], flag1) +
+            W(br, co, rf, com, eid5, vid4, pI[2]).expr + // turn
+            W(br, co, rf, com, eid6, vid4, pI[3]).expr + // turn
+                Eq(Add(eid, Int(4)), eid10) +               // eid update
+                Eq(vid4, Int(0)) + // turn read
+                Eq(Read(rf, eid10), eid5)  + // rf
+                Lt(Read(com, eid5), Read(com, eid10)) +    // com constraint (because rf)
+                Lt(Read(com, eid10), Read(com, eid6)) +    // com constraint (because fr)
+                Eq(Add(Read(co, eid5), Int(1)), Read(co, eid6)) + // co-after is eid6
+                Eq(pI[2], turn) +
+            Or(Eq(turn, Int(1)), Eq(flag1, Int(0))) +
+            W(br, co, rf, com, eid7, vid5, pI[3]).expr + // cnt
+            W(br, co, rf, com, eid8, vid5, pI[4]).expr + // cnt
+                Eq(Add(eid, Int(6)), eid11) +               // eid update
+                Eq(vid5, Int(3)) + // turn
+                Eq(Read(rf, eid11), eid7)  + // rf
+                Lt(Read(com, eid7), Read(com, eid11)) +    // com constraint (because rf)
+                Lt(Read(com, eid11), Read(com, eid8)) +    // com constraint (because fr)
+                Eq(Add(Read(co, eid7), Int(1)), Read(co, eid8)) + // co-after is eid8
+                Eq(pI[3], cnt) +
+            W(br, co, rf, com, eid, vid, pI[0]).expr + // successful write
+                T1G(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr + // previous loc
+                Eq(Add(eid, Int(8)), eid2) +               // eid update
+                Lt(Read(com, eid), Read(com, eid9)) +      // com constraint (because po)
+                Lt(Read(com, eid9), Read(com, eid10)) +    // com constraint (because po)
+                Lt(Read(com, eid10), Read(com, eid11)) +   // com constraint (because po)
+                Lt(Read(com, eid11), Read(com, eid2))      // com constraint (because po)
+
+
+        W(br, co, rf, com, eid, vid, pI[0]) += // cnt := cnt+1
+            W(br, co, rf, com, eid2, vid, pI[1]).expr + // prevW
+                T0C(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr +
+                Eq(vid, Int(3)) +
+                Eq(pI[0], Add(cnt, Int(1))) +
+                Eq(Add(Read(co, eid2), Int(1)), Read(co, eid)) + // co-next
+                Lt(Read(com, eid2), Read(com, eid))
+        W(br, co, rf, com, eid, vid, pI[0]) += // cnt := cnt+1
+            W(br, co, rf, com, eid2, vid, pI[1]).expr + // prevW
+                T1C(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr +
+                Eq(vid, Int(3)) +
+                Eq(pI[0], Add(cnt, Int(1))) +
+                Eq(Add(Read(co, eid2), Int(1)), Read(co, eid)) + // co-next
+                Lt(Read(com, eid2), Read(com, eid))
+
+        T0CF(br, co, rf, com, eid2, turn, flag1, flag2, cnt) +=
+            W(br, co, rf, com, eid, vid, pI[0]).expr + // successful write
+                T0C(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr + // previous loc
+                Eq(Add(eid, Int(2)), eid2) +               // eid update
+                Lt(Read(com, eid), Read(com, eid2))    // com constraint (because po)
+        T1CF(br, co, rf, com, eid2, turn, flag1, flag2, cnt) +=
+            W(br, co, rf, com, eid, vid, pI[0]).expr + // successful write
+                T1C(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr + // previous loc
+                Eq(Add(eid, Int(2)), eid2) +               // eid update
+                Lt(Read(com, eid), Read(com, eid2))    // com constraint (because po)
+
+
+        W(br, co, rf, com, eid, vid, pI[0]) += // cnt := 0
+            W(br, co, rf, com, eid2, vid, pI[1]).expr + // prevW
+                T0CF(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr +
+                Eq(vid, Int(3)) +
+                Eq(pI[0], Int(0)) +
+                Eq(Add(Read(co, eid2), Int(1)), Read(co, eid)) + // co-next
+                Lt(Read(com, eid2), Read(com, eid))
+        W(br, co, rf, com, eid, vid, pI[0]) += // cnt := 0
+            W(br, co, rf, com, eid2, vid, pI[1]).expr + // prevW
+                T1CF(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr +
+                Eq(vid, Int(3)) +
+                Eq(pI[0], Int(0)) +
+                Eq(Add(Read(co, eid2), Int(1)), Read(co, eid)) + // co-next
+                Lt(Read(com, eid2), Read(com, eid))
+
+
+
+        T0F(br, co, rf, com, eid2, turn, flag1, flag2, cnt) +=
+            W(br, co, rf, com, eid, vid, pI[0]).expr + // successful write
+                T0CF(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr + // previous loc
+                Eq(Add(eid, Int(2)), eid2) +               // eid update
+                Lt(Read(com, eid), Read(com, eid2))    // com constraint (because po)
+        T1F(br, co, rf, com, eid2, turn, flag1, flag2, cnt) +=
+            W(br, co, rf, com, eid, vid, pI[0]).expr + // successful write
+                T1CF(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr + // previous loc
+                Eq(Add(eid, Int(2)), eid2) +               // eid update
+                Lt(Read(com, eid), Read(com, eid2))    // com constraint (because po)
+
+
+        W(br, co, rf, com, eid, vid, pI[0]) += // flag1 := 0
+            W(br, co, rf, com, eid2, vid, pI[1]).expr + // prevW
+                T0F(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr +
+                Eq(vid, Int(1)) +
+                Eq(pI[0], Int(0)) +
+                Eq(Add(Read(co, eid2), Int(1)), Read(co, eid)) + // co-next
+                Lt(Read(com, eid2), Read(com, eid))
+        W(br, co, rf, com, eid, vid, pI[0]) += // flag2 := 0
+            W(br, co, rf, com, eid2, vid, pI[1]).expr + // prevW
+                T1F(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr +
+                Eq(vid, Int(2)) +
+                Eq(pI[0], Int(0)) +
+                Eq(Add(Read(co, eid2), Int(1)), Read(co, eid)) + // co-next
+                Lt(Read(com, eid2), Read(com, eid))
+
+        T0(br, co, rf, com, eid2, turn, flag1, flag2, cnt) +=
+            W(br, co, rf, com, eid, vid, pI[0]).expr + // successful write
+                T0F(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr + // previous loc
+                Eq(Add(eid, Int(2)), eid2) +               // eid update
+                Lt(Read(com, eid), Read(com, eid2))    // com constraint (because po)
+        T1(br, co, rf, com, eid, turn, flag1, flag2, cnt) +=
+            W(br, co, rf, com, eid, vid, pI[0]).expr + // successful write
+                T1F(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr + // previous loc
+                Eq(Add(eid, Int(2)), eid2) +               // eid update
+                Lt(Read(com, eid), Read(com, eid2))    // com constraint (because po)
+
+        !(T0C(br, co, rf, com, eid, turn, flag1, flag2, cnt) with Eq(cnt, Int(1)))
+        !(T1C(br, co, rf, com, eid, turn, flag1, flag2, cnt) with Eq(cnt, Int(1)))
+
+        val expr = listOf(init, T0, T0G, T0C, T0CF, T0F, T1, T1G, T1C, T1CF, T1F, W).toSMT2()
+        println(expr)
+    }
+
+
+    @Test
+    fun testPetersonNoCounting() {
+        val i2i = ArrayType.of(Int(), Int())
+
+        val pI = ParamHolder(Int())
+        val pB = ParamHolder(Bool())
+        val pA = ParamHolder(i2i)
+        val br = pA[9]
+        val po = pA[10]
+        val co = pA[11]
+        val rf = pA[12]
+        val com = pA[13]
+        val prevW = pI[14]
+        val eid = pI[15]
+        val eid2 = pI[17]
+        val vid = pI[18]
+        val vid3 = pI[19]
+        val eid3 = pI[20]
+        val eid4 = pI[21]
+        val eid5 = pI[22]
+        val eid6 = pI[23]
+        val vid4 = pI[24]
+        val eid7 = pI[25]
+        val eid8 = pI[26]
+        val vid5 = pI[27]
+        val eid9 = pI[28]
+        val eid10 = pI[29]
+        val eid11 = pI[50]
+
+        val turn = pB[30]
+        val flag1 = pB[31]
+        val flag2 = pB[32]
+        val cnt = pB[33]
+        val turn_old = pB[40]
+        val flag1_old = pB[41]
+        val flag2_old = pB[42]
+
+        val init = Relation("init", i2i, i2i, i2i, i2i, Int()) // br, co, rf, com
+
+        val T0 = Relation("T0", i2i, i2i, i2i, i2i, Int(), Bool(), Bool(), Bool(), Bool()) // br, co, rf, com, eid, turn, flag0, flag1, cnt
+        val T0G = Relation("T0_gate", i2i, i2i, i2i, i2i, Int(), Bool(), Bool(), Bool(), Bool()) // br, co, rf, com, eid, turn, flag0, flag1, cnt
+        val T0C = Relation("T0_critical", i2i, i2i, i2i, i2i, Int(), Bool(), Bool(), Bool(), Bool()) // br, co, rf, com, eid, turn, flag0, flag1, cnt
+        val T0F = Relation("T0_final", i2i, i2i, i2i, i2i, Int(), Bool(), Bool(), Bool(), Bool()) // br, co, rf, com, eid, turn, flag0, flag1, cnt
+
+        val T1 = Relation("T1", i2i, i2i, i2i, i2i, Int(), Bool(), Bool(), Bool(), Bool()) // br, co, rf, com, eid, turn, flag0, flag1, cnt
+        val T1G = Relation("T1_gate", i2i, i2i, i2i, i2i, Int(), Bool(), Bool(), Bool(), Bool()) // br, co, rf, com, eid, turn, flag0, flag1, cnt
+        val T1C = Relation("T1_critical", i2i, i2i, i2i, i2i, Int(), Bool(), Bool(), Bool(), Bool()) // br, co, rf, com, eid, turn, flag0, flag1, cnt
+        val T1F = Relation("T1_final", i2i, i2i, i2i, i2i, Int(), Bool(), Bool(), Bool(), Bool()) // br, co, rf, com, eid, turn, flag0, flag1, cnt
+
+        val W = Relation("W", i2i, i2i, i2i, i2i, Int(), Int(), Bool()) // br, co, rf, com, eid, vid, val
+
+        init(br, co, rf, com, eid) +=
+            Eq(eid, Int(0)) +
+            Eq(Read(co, Int(0)), Int(0)) +
+            Eq(Read(com, Int(0)), Int(0))
+
+        W(br, co, rf, com, eid, vid, pB[0]) += // turn := 0
+            init(br, co, rf, com, eid).expr +
+                Eq(vid, Int(0)) +
+                Eq(pB[0], False())
+        W(br, co, rf, com, eid, vid, pB[0]) += // flag0 := 0
+            init(br, co, rf, com, eid).expr +
+                Eq(vid, Int(1)) +
+                Eq(pB[0], False())
+        W(br, co, rf, com, eid, vid, pB[0]) += // flag1 := 0
+            init(br, co, rf, com, eid).expr +
+                Eq(vid, Int(2)) +
+                Eq(pB[0], False())
+
+        T0(br, co, rf, com, eid, turn, flag1, flag2, cnt) +=
+            init(br, co, rf, com, eid2).expr + Eq(eid, Int(1))
+        T1(br, co, rf, com, eid, turn, flag1, flag2, cnt) +=
+            init(br, co, rf, com, eid2).expr + Eq(eid, Int(2))
+
+        W(br, co, rf, com, eid, vid, pB[0]) += // flag0 := 1
+            W(br, co, rf, com, eid2, vid, pB[1]).expr + // prevW
+            T0(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr +
+                Eq(vid, Int(1)) +
+                Eq(pB[0], True()) +
+                Eq(Add(Read(co, eid2), Int(1)), Read(co, eid)) + // co-next
+                Lt(Read(com, eid2), Read(com, eid))
+        W(br, co, rf, com, eid, vid, pB[0]) += // flag1 := 1
+            W(br, co, rf, com, eid2, vid, pB[1]).expr + // prevW
+            T1(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr +
+                Eq(vid, Int(2)) +
+                Eq(pB[0], True()) +
+                Eq(Add(Read(co, eid2), Int(1)), Read(co, eid)) + // co-next
+                Lt(Read(com, eid2), Read(com, eid))
+
+        T0G(br, co, rf, com, eid2, turn, flag1, flag2, cnt) +=
+            W(br, co, rf, com, eid, vid, pB[0]).expr + // successful write
+            T0(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr + // previous loc
+                Eq(Add(eid, Int(2)), eid2) +               // eid update
+                Lt(Read(com, eid), Read(com, eid2))    // com constraint (because po)
+        T1G(br, co, rf, com, eid2, turn, flag1, flag2, cnt) +=
+            W(br, co, rf, com, eid, vid, pB[0]).expr + // successful write
+                T1(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr + // previous loc
+                Eq(Add(eid, Int(2)), eid2) +               // eid update
+                Lt(Read(com, eid), Read(com, eid2))    // com constraint (because po)
+
+        W(br, co, rf, com, eid, vid, pB[0]) += // turn := 1
+            W(br, co, rf, com, eid2, vid, pB[1]).expr + // prevW
+                T0G(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr +
+                Eq(vid, Int(0)) +
+                Eq(pB[0], True()) +
+                Eq(Add(Read(co, eid2), Int(1)), Read(co, eid)) + // co-next
+                Lt(Read(com, eid2), Read(com, eid))
+        W(br, co, rf, com, eid, vid, pB[0]) += // turn := 0
+            W(br, co, rf, com, eid2, vid, pB[1]).expr + // prevW
+                T1G(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr +
+                Eq(vid, Int(0)) +
+                Eq(pB[0], False()) +
+                Eq(Add(Read(co, eid2), Int(1)), Read(co, eid)) + // co-next
+                Lt(Read(com, eid2), Read(com, eid))
+
+        T0C(br, co, rf, com, eid2, turn, flag1, flag2, cnt) +=
+            W(br, co, rf, com, eid3, vid3, pB[1]).expr + // rf-source
+            W(br, co, rf, com, eid4, vid3, pB[2]).expr + // rf-source
+                Eq(Add(eid, Int(2)), eid9) +               // eid update
+                Eq(vid3, Int(2)) + // flag[1] read
+                Eq(Read(rf, eid3), eid9) + // rf
+                Lt(Read(com, eid3), Read(com, eid9)) +    // com constraint (because rf)
+                Lt(Read(com, eid9), Read(com, eid4)) +    // com constraint (because fr)
+                Eq(Add(Read(co, eid3), Int(1)), Read(co, eid4)) + // co-after is eid4
+                Eq(pB[1], flag2) +
+            W(br, co, rf, com, eid5, vid4, pB[2]).expr + // turn
+            W(br, co, rf, com, eid6, vid4, pB[3]).expr + // turn
+                Eq(Add(eid, Int(4)), eid10) +               // eid update
+                Eq(vid4, Int(0)) + // turn read
+                Eq(Read(rf, eid10), eid5)  + // rf
+                Lt(Read(com, eid5), Read(com, eid10)) +    // com constraint (because rf)
+                Lt(Read(com, eid10), Read(com, eid6)) +    // com constraint (because fr)
+                Eq(Add(Read(co, eid5), Int(1)), Read(co, eid6)) + // co-after is eid6
+                Eq(pB[2], turn) +
+            Or(Not(turn), Not(flag2)) +
+            W(br, co, rf, com, eid, vid, pB[0]).expr + // successful write
+                T0G(br, co, rf, com, eid, turn_old, flag1, flag2_old, cnt).expr + // previous loc
+                Eq(Add(eid, Int(6)), eid2) +               // eid update
+                Lt(Read(com, eid), Read(com, eid9)) +      // com constraint (because po)
+                Lt(Read(com, eid9), Read(com, eid10)) +    // com constraint (because po)
+                Lt(Read(com, eid10), Read(com, eid2))    // com constraint (because po)
+
+        T1C(br, co, rf, com, eid2, turn, flag1, flag2, cnt) +=
+            W(br, co, rf, com, eid3, vid3, pB[1]).expr + // rf-source
+            W(br, co, rf, com, eid4, vid3, pB[2]).expr + // rf-source
+                Eq(Add(eid, Int(2)), eid9) +               // eid update
+                Eq(vid3, Int(1)) + // flag[0] read
+                Eq(Read(rf, eid9), eid3) + // rf
+                Lt(Read(com, eid3), Read(com, eid9)) +    // com constraint (because rf)
+                Lt(Read(com, eid9), Read(com, eid4)) +    // com constraint (because fr)
+                Eq(Add(Read(co, eid3), Int(1)), Read(co, eid4)) + // co-after is eid4
+                Eq(pB[1], flag1) +
+            W(br, co, rf, com, eid5, vid4, pB[2]).expr + // turn
+            W(br, co, rf, com, eid6, vid4, pB[3]).expr + // turn
+                Eq(Add(eid, Int(4)), eid10) +               // eid update
+                Eq(vid4, Int(0)) + // turn read
+                Eq(Read(rf, eid10), eid5)  + // rf
+                Lt(Read(com, eid5), Read(com, eid10)) +    // com constraint (because rf)
+                Lt(Read(com, eid10), Read(com, eid6)) +    // com constraint (because fr)
+                Eq(Add(Read(co, eid5), Int(1)), Read(co, eid6)) + // co-after is eid6
+                Eq(pB[2], turn) +
+            Or(turn, Not(flag1)) +
+            W(br, co, rf, com, eid, vid, pB[0]).expr + // successful write
+                T1G(br, co, rf, com, eid, turn_old, flag1_old, flag2, cnt).expr + // previous loc
+                Eq(Add(eid, Int(6)), eid2) +               // eid update
+                Lt(Read(com, eid), Read(com, eid9)) +      // com constraint (because po)
+                Lt(Read(com, eid9), Read(com, eid10)) +    // com constraint (because po)
+                Lt(Read(com, eid10), Read(com, eid2))      // com constraint (because po)
+
+        T0F(br, co, rf, com, eid2, turn, flag1, flag2, cnt) +=
+            T0C(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr + // previous loc
+            Eq(Add(eid, Int(2)), eid2) +               // eid update
+            Lt(Read(com, eid), Read(com, eid2))    // com constraint (because po)
+        T1F(br, co, rf, com, eid2, turn, flag1, flag2, cnt) +=
+            T1C(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr + // previous loc
+            Eq(Add(eid, Int(2)), eid2) +               // eid update
+            Lt(Read(com, eid), Read(com, eid2))    // com constraint (because po)
+
+
+        W(br, co, rf, com, eid, vid, pB[0]) += // cnt := 0
+            W(br, co, rf, com, eid2, vid, pB[1]).expr + // prevW
+                T0F(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr +
+                Eq(vid, Int(1)) +
+                Eq(pB[0], False()) +
+                Eq(Add(Read(co, eid2), Int(1)), Read(co, eid)) + // co-next
+                Lt(Read(com, eid2), Read(com, eid))
+        W(br, co, rf, com, eid, vid, pB[0]) += // cnt := 0
+            W(br, co, rf, com, eid2, vid, pB[1]).expr + // prevW
+                T1F(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr +
+                Eq(vid, Int(2)) +
+                Eq(pB[0], False()) +
+                Eq(Add(Read(co, eid2), Int(1)), Read(co, eid)) + // co-next
+                Lt(Read(com, eid2), Read(com, eid))
+
+//        T0(br, co, rf, com, eid2, turn, flag1, flag2, cnt) +=
+//            W(br, co, rf, com, eid, vid, pB[0]).expr + // successful write
+//                T0F(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr + // previous loc
+//                Eq(Add(eid, Int(2)), eid2) +               // eid update
+//                Lt(Read(com, eid), Read(com, eid2))    // com constraint (because po)
+//        T1(br, co, rf, com, eid, turn, flag1, flag2, cnt) +=
+//            W(br, co, rf, com, eid, vid, pB[0]).expr + // successful write
+//                T1F(br, co, rf, com, eid, turn, flag1, flag2, cnt).expr + // previous loc
+//                Eq(Add(eid, Int(2)), eid2) +               // eid update
+//                Lt(Read(com, eid), Read(com, eid2))    // com constraint (because po)
+
+        !(T0C(br, co, rf, com, eid, turn, flag1, flag2, cnt) with
+            T1C(br, co, rf, com, eid2, turn_old, flag1_old, flag2_old, cnt).expr +
+                Eq(Read(com, eid), Read(com, eid2)))
+
+        val expr = listOf(init, T0, T0G, T0C, T0F, T1, T1G, T1C, T1F, W).toSMT2()
+        println(expr)
+    }
+
+}