diff --git a/build.gradle.kts b/build.gradle.kts
index 4c4802c7ba..4a69da4502 100644
--- a/build.gradle.kts
+++ b/build.gradle.kts
@@ -12,7 +12,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "4.2.5"
+    version = "4.3.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }
diff --git a/scripts/starexec_run_default.sh b/scripts/starexec_run_default.sh
new file mode 100755
index 0000000000..dc098f683c
--- /dev/null
+++ b/scripts/starexec_run_default.sh
@@ -0,0 +1,33 @@
+#!/bin/bash
+scriptdir=$(dirname $(realpath "$0"))
+
+JAVA_FALLBACK_PATH="/usr/lib/jvm/java-17/bin/java"
+JAVA=$(java --version 2>&1 | grep "openjdk 17" >/dev/null && echo "java" || echo $JAVA_FALLBACK_PATH)
+$JAVA --version >/dev/null || exit
+
+input="$1"
+output="$2/$(basename $1 smt2)out"
+
+configurations=("--domain PRED_SPLIT --refinement BW_BIN_ITP --predsplit WHOLE"
+				"--domain PRED_CART --refinement BW_BIN_ITP --predsplit WHOLE"
+				"--domain EXPL --refinement SEQ_ITP")
+
+SECONDS=0
+
+for i in ${!configurations[@]}; do
+    flags=${configurations[$i]}
+    remaining=$(((1800-$SECONDS)/(3-i)))
+    echo "Running config ($i) for $remaining seconds..." >> "$output"
+    echo LD_LIBRARY_PATH=$scriptdir/../lib $JAVA -Xss120m -Xmx28G -Dfile.encoding=UTF-8 -jar $scriptdir/../theta.jar --chc --input $1 $flags --maxenum 1 --initprec EMPTY --smt-home $scriptdir/../solvers --loglevel RESULT >> "$output"
+	result=$(LD_LIBRARY_PATH=$scriptdir/../lib timeout $remaining $JAVA -Xss120m -Xmx28G -Dfile.encoding=UTF-8 -jar $scriptdir/../theta.jar --chc --input $1 $flags --maxenum 1 --initprec EMPTY --smt-home $scriptdir/../solvers --loglevel RESULT 2>&1 | tee -a "$output" | grep SafetyResult)
+
+	if [[ $result == *"Unsafe"* ]]; then
+		echo "unsat"
+		exit
+	elif [[ $result == *"Safe"* ]]; then
+		echo "sat"
+		exit
+	fi
+done
+
+echo "unknown"
diff --git a/settings.gradle.kts b/settings.gradle.kts
index 9ca2669819..725c2149f7 100644
--- a/settings.gradle.kts
+++ b/settings.gradle.kts
@@ -7,6 +7,7 @@ include(
         "common/grammar",
 
         "frontends/c-frontend",
+        "frontends/chc-frontend",
 
         "cfa/cfa",
         "cfa/cfa-analysis",
diff --git a/subprojects/frontends/chc-frontend/build.gradle.kts b/subprojects/frontends/chc-frontend/build.gradle.kts
new file mode 100644
index 0000000000..5f6c8c257b
--- /dev/null
+++ b/subprojects/frontends/chc-frontend/build.gradle.kts
@@ -0,0 +1,11 @@
+plugins {
+    id("java-common")
+    id("antlr-grammar")
+}
+
+dependencies {
+    implementation(project(":theta-core"))
+    implementation(project(":theta-common"))
+    implementation(project(":theta-xcfa"))
+    implementation(project(":theta-solver-smtlib"))
+}
diff --git a/subprojects/frontends/chc-frontend/src/main/antlr/CHC.g4 b/subprojects/frontends/chc-frontend/src/main/antlr/CHC.g4
new file mode 100644
index 0000000000..41fe637466
--- /dev/null
+++ b/subprojects/frontends/chc-frontend/src/main/antlr/CHC.g4
@@ -0,0 +1,1158 @@
+/**
+ * SMT-LIB (v2.6) grammar
+ *
+ * Grammar is baesd on the following specification:
+ * http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf
+ *
+ * The MIT License (MIT)
+ *
+ * Copyright (c) 2017 Julian Thome <julian.thome.de@gmail.com>
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+ * of the Software, and to permit persons to whom the Software is furnished to do
+ * so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ * SOFTWARE.
+ **/
+
+grammar CHC;
+
+
+// Lexer Rules Start
+
+
+Comment
+    : Semicolon ~[\r\n]* -> skip
+    ;
+
+
+ParOpen
+    : '('
+    ;
+
+ParClose
+    : ')'
+    ;
+
+Semicolon
+    : ';'
+    ;
+
+String
+    : '"' (PrintableCharNoDquote | WhiteSpaceChar)+ '"'
+    ;
+
+QuotedSymbol:
+    '|' (PrintableCharNoBackslash | WhiteSpaceChar)+ '|'
+    ;
+Arrow
+    : '=>'
+    ;
+
+// Predefined Symbols
+
+PS_Not
+    : 'not'
+    ;
+PS_And
+    : 'and'
+    ;
+PS_Bool
+    : 'Bool'
+    ;
+PS_ContinuedExecution
+    : 'continued-execution'
+    ;
+PS_Error
+    : 'error'
+    ;
+PS_False
+    : 'false'
+    ;
+PS_ImmediateExit
+    : 'immediate-exit'
+    ;
+PS_Incomplete
+    : 'incomplete'
+    ;
+PS_Logic
+    : 'logic'
+    ;
+PS_Memout
+    : 'memout'
+    ;
+PS_Sat
+    : 'sat'
+    ;
+PS_Success
+    : 'success'
+    ;
+PS_Theory
+    : 'theory'
+    ;
+PS_True
+    : 'true'
+    ;
+PS_Unknown
+    : 'unknown'
+    ;
+PS_Unsupported
+    : 'unsupported'
+    ;
+PS_Unsat
+    : 'unsat'
+    ;
+
+// RESERVED Words
+
+// Command names
+
+
+CMD_Assert
+    : 'assert'
+    ;
+CMD_CheckSat
+    : 'check-sat'
+    ;
+CMD_CheckSatAssuming
+    : 'check-sat-assuming'
+    ;
+CMD_DeclareConst
+    : 'declare-const'
+    ;
+CMD_DeclareDatatype
+    : 'declare-datatype'
+    ;
+CMD_DeclareDatatypes
+    : 'declare-datatypes'
+    ;
+CMD_DeclareFun
+    : 'declare-fun'
+    ;
+CMD_DeclareSort
+    : 'declare-sort'
+    ;
+CMD_DefineFun
+    : 'define-fun'
+    ;
+CMD_DefineFunRec
+    : 'define-fun-rec'
+    ;
+CMD_DefineFunsRec
+    : 'define-funs-rec'
+    ;
+CMD_DefineSort
+    : 'define-sort'
+    ;
+CMD_Echo
+    : 'echo'
+    ;
+CMD_Exit
+    : 'exit'
+    ;
+CMD_GetAssertions
+    : 'get-assertions'
+    ;
+CMD_GetAssignment
+    : 'get-assignment'
+    ;
+CMD_GetInfo
+    : 'get-info'
+    ;
+CMD_GetModel
+    : 'get-model'
+    ;
+CMD_GetOption
+    : 'get-option'
+    ;
+CMD_GetProof
+    : 'get-proof'
+    ;
+CMD_GetUnsatAssumptions
+    : 'get-unsat-assumptions'
+    ;
+CMD_GetUnsatCore
+    : 'get-unsat-core'
+    ;
+CMD_GetValue
+    : 'get-value'
+    ;
+CMD_Pop
+    : 'pop'
+    ;
+CMD_Push
+    : 'push'
+    ;
+CMD_Reset
+    : 'reset'
+    ;
+CMD_ResetAssertions
+    : 'reset-assertions'
+    ;
+CMD_SetInfo
+    : 'set-info'
+    ;
+CMD_SetLogic
+    : 'set-logic'
+    ;
+CMD_SetOption
+    : 'set-option'
+    ;
+
+
+
+
+// General reserved words
+
+GRW_Exclamation
+    : '!'
+    ;
+GRW_Underscore
+    : '_'
+    ;
+GRW_As
+    : 'as'
+    ;
+GRW_Binary
+    : 'BINARY'
+    ;
+GRW_Decimal
+    : 'DECIMAL'
+    ;
+GRW_Exists
+    : 'exists'
+    ;
+GRW_Hexadecimal
+    : 'HEXADECIMAL'
+    ;
+GRW_Forall
+    : 'forall'
+    ;
+GRW_Let
+    : 'let'
+    ;
+GRW_Match
+    : 'match'
+    ;
+GRW_Numeral
+    : 'NUMERAL'
+    ;
+GRW_Par
+    : 'par'
+    ;
+GRW_String
+    : 'string'
+    ;
+
+Numeral
+    : '0'
+    | [1-9] Digit*
+    ;
+
+Binary
+    : '#b' BinaryDigit+
+    ;
+
+HexDecimal
+    : '#x' HexDigit+
+    ;
+
+Decimal
+    : Numeral '.' '0'* Numeral
+    ;
+
+
+
+fragment HexDigit
+    : '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
+    ;
+
+
+Colon
+    : ':'
+    ;
+
+fragment Digit
+    : [0-9]
+    ;
+
+fragment Letter
+    : 'a'..'z'
+    | 'A' .. 'Z'
+    | '_'
+    ;
+
+fragment Sym
+    : Letter
+    | '+'
+    | '='
+    | '/'
+    | '*'
+    | '%'
+    | '?'
+    | '!'
+    | '$'
+    | '-'
+    | '~'
+    | '&'
+    | '^'
+    | '<'
+    | '>'
+    | '@'
+    | '.'
+    ;
+
+
+
+fragment BinaryDigit
+    : [01]
+    ;
+
+fragment PrintableChar
+    : '\u0020' .. '\u007E'
+    | '\u0080' .. '\uffff'
+    | EscapedSpace
+    ;
+
+fragment PrintableCharNoDquote
+    : '\u0020' .. '\u0021'
+    | '\u0023' .. '\u007E'
+    | '\u0080' .. '\uffff'
+    | EscapedSpace
+    ;
+
+fragment PrintableCharNoBackslash
+    : '\u0020' .. '\u005B'
+    | '\u005D' .. '\u007B'
+    | '\u007D' .. '\u007E'
+    | '\u0080' .. '\uffff'
+    | EscapedSpace
+    ;
+
+fragment EscapedSpace
+    : '""'
+    ;
+
+fragment WhiteSpaceChar
+    : '\u0009'
+    | '\u000A'
+    | '\u000D'
+    | '\u0020'
+    ;
+
+// Lexer Rules End
+
+// Predefined Keywords
+
+
+
+PK_AllStatistics
+    : ':all-statistics'
+    ;
+PK_AssertionStackLevels
+    : ':assertion-stack-levels'
+    ;
+PK_Authors
+    : ':authors'
+    ;
+PK_Category
+    : ':category'
+    ;
+PK_Chainable
+    : ':chainable'
+    ;
+PK_Definition
+    : ':definition'
+    ;
+PK_DiagnosticOutputChannel
+    : ':diagnostic-output-channel'
+    ;
+PK_ErrorBehaviour
+    : ':error-behavior'
+    ;
+PK_Extension
+    : ':extensions'
+    ;
+PK_Funs
+    : ':funs'
+    ;
+PK_FunsDescription
+    : ':funs-description'
+    ;
+PK_GlobalDeclarations
+    : ':global-declarations'
+    ;
+PK_InteractiveMode
+    : ':interactive-mode'
+    ;
+PK_Language
+    : ':language'
+    ;
+PK_LeftAssoc
+    : ':left-assoc'
+    ;
+PK_License
+    : ':license'
+    ;
+PK_Named
+    : ':named'
+    ;
+PK_Name
+    : ':name'
+    ;
+PK_Notes
+    : ':notes'
+    ;
+PK_Pattern
+    : ':pattern'
+    ;
+PK_PrintSuccess
+    : ':print-success'
+    ;
+PK_ProduceAssertions
+    : ':produce-assertions'
+    ;
+PK_ProduceAssignments
+    : ':produce-assignments'
+    ;
+PK_ProduceModels
+    : ':produce-models'
+    ;
+PK_ProduceProofs
+    : ':produce-proofs'
+    ;
+PK_ProduceUnsatAssumptions
+    : ':produce-unsat-assumptions'
+    ;
+PK_ProduceUnsatCores
+    : ':produce-unsat-cores'
+    ;
+PK_RandomSeed
+    : ':random-seed'
+    ;
+PK_ReasonUnknown
+    : ':reason-unknown'
+    ;
+PK_RegularOutputChannel
+    : ':regular-output-channel'
+    ;
+PK_ReproducibleResourceLimit
+    : ':reproducible-resource-limit'
+    ;
+PK_RightAssoc
+    : ':right-assoc'
+    ;
+PK_SmtLibVersion
+    : ':smt-lib-version'
+    ;
+PK_Sorts
+    : ':sorts'
+    ;
+PK_SortsDescription
+    : ':sorts-description'
+    ;
+PK_Source
+    : ':source'
+    ;
+PK_Status
+    : ':status'
+    ;
+PK_Theories
+    : ':theories'
+    ;
+PK_Values
+    : ':values'
+    ;
+PK_Verbosity
+    : ':verbosity'
+    ;
+PK_Version
+    : ':version'
+    ;
+
+Name:
+    (Letter|Digit) (Digit | Sym)*;
+
+UndefinedSymbol:
+    Sym (Digit | Sym)*;
+
+
+
+// Parser Rules Start
+
+// Starting rule(s)
+
+start
+    : benchmark EOF
+    ;
+
+response
+    : general_response EOF
+    ;
+
+generalReservedWord
+    : GRW_Exclamation
+    | GRW_Underscore
+    | GRW_As
+    | GRW_Binary
+    | GRW_Decimal
+    | GRW_Exists
+    | GRW_Hexadecimal
+    | GRW_Forall
+    | GRW_Let
+    | GRW_Match
+    | GRW_Numeral
+    | GRW_Par
+    | GRW_String
+    ;
+
+
+simpleSymbol
+    : predefSymbol
+    | UndefinedSymbol
+    | Name
+    ;
+
+quotedSymbol
+    : QuotedSymbol
+    ;
+
+predefSymbol
+    : PS_Not
+    | PS_And
+    | PS_Bool
+    | PS_ContinuedExecution
+    | PS_Error
+    | PS_False
+    | PS_ImmediateExit
+    | PS_Incomplete
+    | PS_Logic
+    | PS_Memout
+    | PS_Sat
+    | PS_Success
+    | PS_Theory
+    | PS_True
+    | PS_Unknown
+    | PS_Unsupported
+    | PS_Unsat
+    ;
+
+predefKeyword
+    : PK_AllStatistics
+    | PK_AssertionStackLevels
+    | PK_Authors
+    | PK_Category
+    | PK_Chainable
+    | PK_Definition
+    | PK_DiagnosticOutputChannel
+    | PK_ErrorBehaviour
+    | PK_Extension
+    | PK_Funs
+    | PK_FunsDescription
+    | PK_GlobalDeclarations
+    | PK_InteractiveMode
+    | PK_Language
+    | PK_LeftAssoc
+    | PK_License
+    | PK_Named
+    | PK_Name
+    | PK_Notes
+    | PK_Pattern
+    | PK_PrintSuccess
+    | PK_ProduceAssertions
+    | PK_ProduceAssignments
+    | PK_ProduceModels
+    | PK_ProduceProofs
+    | PK_ProduceUnsatAssumptions
+    | PK_ProduceUnsatCores
+    | PK_RandomSeed
+    | PK_ReasonUnknown
+    | PK_RegularOutputChannel
+    | PK_ReproducibleResourceLimit
+    | PK_RightAssoc
+    | PK_SmtLibVersion
+    | PK_Sorts
+    | PK_SortsDescription
+    | PK_Source
+    | PK_Status
+    | PK_Theories
+    | PK_Values
+    | PK_Verbosity
+    | PK_Version
+    ;
+
+
+
+symbol
+    : simpleSymbol
+    | quotedSymbol
+    ;
+
+numeral
+    : Numeral
+    ;
+
+decimal
+    : Decimal
+    ;
+
+hexadecimal
+    : HexDecimal
+    ;
+
+binary
+    : Binary
+    ;
+
+string
+    : String
+    ;
+
+keyword
+    : predefKeyword
+    | Colon simpleSymbol
+    ;
+
+// S-expression
+
+spec_constant
+    : numeral
+    | decimal
+    | hexadecimal
+    | binary
+    | string
+    ;
+
+
+s_expr
+    : spec_constant
+    | symbol
+    | keyword
+    | ParOpen s_expr* ParClose
+    ;
+
+// Identifiers
+
+index
+    : numeral
+    | symbol
+    ;
+
+identifier
+    : symbol
+    | ParOpen GRW_Underscore symbol index+ ParClose
+    ;
+
+// Attributes
+
+attribute_value
+    : spec_constant
+    | symbol
+    | ParOpen s_expr* ParClose
+    ;
+
+attribute
+    : keyword
+    | keyword attribute_value
+    ;
+
+// Sorts
+
+sort
+    : identifier
+    | ParOpen identifier sort+ ParClose
+    ;
+
+
+// Terms and Formulas
+
+qual_identifier
+    : identifier
+    | ParOpen GRW_As identifier sort ParClose
+    ;
+
+var_binding
+    : ParOpen symbol term ParClose
+    ;
+
+sorted_var
+    : ParOpen symbol sort ParClose
+    ;
+
+pattern
+    : symbol
+    | ParOpen symbol symbol+ ParClose
+    ;
+
+match_case
+    : ParOpen pattern term ParClose
+    ;
+
+term
+    : spec_constant
+    | qual_identifier
+    | ParOpen qual_identifier term+ ParClose
+    | ParOpen GRW_Let ParOpen var_binding+ ParClose term ParClose
+    | ParOpen GRW_Forall ParOpen sorted_var+ ParClose term ParClose
+    | ParOpen GRW_Exists ParOpen sorted_var+ ParClose term ParClose
+    | ParOpen GRW_Match term ParOpen match_case+ ParClose ParClose
+    | ParOpen GRW_Exclamation term attribute+ ParClose
+    ;
+
+
+// Theory Declarations
+
+sort_symbol_decl
+    : ParOpen identifier numeral attribute* ParClose;
+
+meta_spec_constant
+    : GRW_Numeral
+    | GRW_Decimal
+    | GRW_String
+    ;
+
+fun_symbol_decl
+    : ParOpen spec_constant sort attribute* ParClose
+    | ParOpen meta_spec_constant sort attribute* ParClose
+    | ParOpen identifier sort+ attribute* ParClose
+    ;
+
+par_fun_symbol_decl
+    : fun_symbol_decl
+    | ParOpen GRW_Par ParOpen symbol+ ParClose ParOpen identifier sort+
+    attribute* ParClose ParClose
+    ;
+
+theory_attribute
+    : PK_Sorts ParOpen sort_symbol_decl+ ParClose
+    | PK_Funs ParOpen par_fun_symbol_decl+ ParClose
+    | PK_SortsDescription string
+    | PK_FunsDescription string
+    | PK_Definition string
+    | PK_Values string
+    | PK_Notes string
+    | attribute
+    ;
+
+theory_decl
+    : ParOpen PS_Theory symbol theory_attribute+ ParClose
+    ;
+
+
+// Logic Declarations
+
+logic_attribue
+    : PK_Theories ParOpen symbol+ ParClose
+    | PK_Language string
+    | PK_Extension string
+    | PK_Values string
+    | PK_Notes string
+    | attribute
+    ;
+
+logic
+    : ParOpen PS_Logic symbol logic_attribue+ ParClose
+    ;
+
+
+// Scripts
+
+sort_dec
+    : ParOpen symbol numeral ParClose
+    ;
+
+selector_dec
+    : ParOpen symbol sort ParClose
+    ;
+
+constructor_dec
+    : ParOpen symbol selector_dec* ParClose
+    ;
+
+datatype_dec
+    : ParOpen constructor_dec+ ParClose
+    | ParOpen GRW_Par ParOpen symbol+ ParClose ParOpen constructor_dec+
+    ParClose ParClose
+    ;
+
+function_dec
+    : ParOpen symbol ParOpen sorted_var* ParClose sort ParClose
+    ;
+
+function_def
+    : symbol ParOpen sorted_var* ParClose sort term
+    ;
+
+prop_literal
+    : symbol
+    | ParOpen PS_Not symbol ParClose
+    ;
+
+// CHC
+benchmark:
+    (ParOpen cmd_setInfo attribute ParClose)*
+    horn_logic
+    (ParOpen cmd_setInfo attribute ParClose)*
+    fun_decl+
+    (ParOpen CMD_Assert chc_assert ParClose)*
+    ParOpen CMD_Assert chc_query ParClose
+    ParOpen CMD_CheckSat ParClose
+    (ParOpen CMD_Exit ParClose)?
+    ;
+
+horn_logic: ParOpen CMD_SetLogic 'HORN' ParClose;
+fun_decl: ParOpen CMD_DeclareFun symbol ParOpen sort* ParClose PS_Bool ParClose;
+
+chc_assert // a well-formed first-order sentence of the form
+    : ParOpen GRW_Forall ParOpen var_decl+ ParClose ParOpen Arrow chc_tail chc_head ParClose ParClose
+    | ParOpen GRW_Forall ParOpen var_decl+ ParClose chc_head ParClose
+    | u_predicate
+    ;
+
+var_decl: ParOpen symbol sort ParClose;
+
+chc_head: u_pred_atom; // where all argument variables in the atom are DISTINCT
+
+chc_tail
+    : u_pred_atom
+    | ParOpen PS_And u_pred_atom+ i_formula* ParClose
+    | i_formula
+    ;
+
+u_pred_atom
+    : u_predicate                           // nullary predicate
+    | ParOpen u_predicate symbol* ParClose  // predicate with arguments
+    ;
+
+// a well-formed first-order sentence of the form
+chc_query: ParOpen GRW_Forall ParOpen var_decl+ ParClose ParOpen Arrow chc_tail PS_False ParClose ParClose;
+
+// uninterpreted predicate (i.e., Boolean function)
+u_predicate
+    : Name
+    | QuotedSymbol
+    ;
+
+// an SMT-LIB formula over variables, and interpreted functions and predicate
+i_formula: term;
+
+
+script
+    : command*
+    ;
+
+cmd_assert
+    : CMD_Assert
+    ;
+
+cmd_checkSat
+    : CMD_CheckSat
+    ;
+
+cmd_checkSatAssuming
+    : CMD_CheckSatAssuming
+    ;
+
+cmd_declareConst
+    : CMD_DeclareConst
+    ;
+
+cmd_declareDatatype
+    : CMD_DeclareDatatype
+    ;
+
+cmd_declareDatatypes
+    : CMD_DeclareDatatypes
+    ;
+
+cmd_declareFun
+    : CMD_DeclareFun
+    ;
+
+cmd_declareSort
+    : CMD_DeclareSort
+    ;
+
+cmd_defineFun
+    : CMD_DefineFun
+    ;
+
+cmd_defineFunRec
+    : CMD_DefineFunRec
+    ;
+
+cmd_defineFunsRec
+    : CMD_DefineFunsRec
+    ;
+
+cmd_defineSort
+    : CMD_DefineSort
+    ;
+
+cmd_echo
+    : CMD_Echo
+    ;
+
+cmd_exit
+    : CMD_Exit
+    ;
+
+cmd_getAssertions
+    : CMD_GetAssertions
+    ;
+
+cmd_getAssignment
+    : CMD_GetAssignment
+    ;
+
+cmd_getInfo
+    : CMD_GetInfo
+    ;
+
+cmd_getModel
+    : CMD_GetModel
+    ;
+
+cmd_getOption
+    : CMD_GetOption
+    ;
+
+cmd_getProof
+    : CMD_GetProof
+    ;
+
+cmd_getUnsatAssumptions
+    : CMD_GetUnsatAssumptions
+    ;
+
+cmd_getUnsatCore
+    : CMD_GetUnsatCore
+    ;
+
+cmd_getValue
+    : CMD_GetValue
+    ;
+
+cmd_pop
+    : CMD_Pop
+    ;
+
+cmd_push
+    : CMD_Push
+    ;
+
+cmd_reset
+    : CMD_Reset
+    ;
+
+cmd_resetAssertions
+    : CMD_ResetAssertions
+    ;
+
+cmd_setInfo
+    : CMD_SetInfo
+    ;
+
+cmd_setLogic
+    : CMD_SetLogic
+    ;
+
+cmd_setOption
+    : CMD_SetOption
+    ;
+
+command
+    : ParOpen cmd_assert term ParClose
+    | ParOpen cmd_checkSat ParClose
+    | ParOpen cmd_checkSatAssuming ParClose
+    | ParOpen cmd_declareConst symbol sort ParClose
+    | ParOpen cmd_declareDatatype symbol datatype_dec ParClose
+    // cardinalitiees for sort_dec and datatype_dec have to be n+1
+    | ParOpen cmd_declareDatatypes ParOpen sort_dec+ ParClose ParOpen
+    datatype_dec+ ParClose ParClose
+    | ParOpen cmd_declareFun symbol ParOpen sort* ParClose sort ParClose
+    | ParOpen cmd_declareSort symbol numeral ParClose
+    | ParOpen cmd_defineFun function_def ParClose
+    | ParOpen cmd_defineFunRec function_def ParClose
+    // cardinalitiees for function_dec and term have to be n+1
+    | ParOpen cmd_defineFunsRec ParOpen function_dec+ ParClose
+    ParOpen term+ ParClose ParClose
+    | ParOpen cmd_defineSort symbol ParOpen symbol* ParClose sort ParClose
+    | ParOpen cmd_echo string ParClose
+    | ParOpen cmd_exit ParClose
+    | ParOpen cmd_getAssertions ParClose
+    | ParOpen cmd_getAssignment ParClose
+    | ParOpen cmd_getInfo info_flag ParClose
+    | ParOpen cmd_getModel ParClose
+    | ParOpen cmd_getOption keyword ParClose
+    | ParOpen cmd_getProof ParClose
+    | ParOpen cmd_getUnsatAssumptions ParClose
+    | ParOpen cmd_getUnsatCore ParClose
+    | ParOpen cmd_getValue ParOpen term+ ParClose ParClose
+    | ParOpen cmd_pop numeral ParClose
+    | ParOpen cmd_push numeral ParClose
+    | ParOpen cmd_reset ParClose
+    | ParOpen cmd_resetAssertions ParClose
+    | ParOpen cmd_setInfo attribute ParClose
+    | ParOpen cmd_setLogic symbol ParClose
+    | ParOpen cmd_setOption option ParClose
+    ;
+
+
+b_value
+    : PS_True
+    | PS_False
+    ;
+
+option
+    : PK_DiagnosticOutputChannel string
+    | PK_GlobalDeclarations b_value
+    | PK_InteractiveMode b_value
+    | PK_PrintSuccess b_value
+    | PK_ProduceAssertions b_value
+    | PK_ProduceAssignments b_value
+    | PK_ProduceModels b_value
+    | PK_ProduceProofs b_value
+    | PK_ProduceUnsatAssumptions b_value
+    | PK_ProduceUnsatCores b_value
+    | PK_RandomSeed numeral
+    | PK_RegularOutputChannel string
+    | PK_ReproducibleResourceLimit numeral
+    | PK_Verbosity numeral
+    | attribute
+    ;
+
+info_flag
+    : PK_AllStatistics
+    | PK_AssertionStackLevels
+    | PK_Authors
+    | PK_ErrorBehaviour
+    | PK_Name
+    | PK_ReasonUnknown
+    | PK_Version
+    | keyword
+    ;
+
+// responses
+
+error_behaviour
+    : PS_ImmediateExit
+    | PS_ContinuedExecution
+    ;
+
+reason_unknown
+    : PS_Memout
+    | PS_Incomplete
+    | s_expr
+    ;
+
+model_response
+    : ParOpen CMD_DefineFun function_def ParClose
+    | ParOpen CMD_DefineFunRec function_def ParClose
+    // cardinalitiees for function_dec and term have to be n+1
+    | ParOpen CMD_DefineFunsRec ParOpen function_dec+ ParClose ParOpen term+
+    ParClose ParClose
+    ;
+
+info_response
+    : PK_AssertionStackLevels numeral
+    | PK_Authors string
+    | PK_ErrorBehaviour error_behaviour
+    | PK_Name string
+    | PK_ReasonUnknown reason_unknown
+    | PK_Version string
+    | attribute
+    ;
+
+valuation_pair
+    : ParOpen term term ParClose
+    ;
+
+t_valuation_pair
+    : ParOpen symbol b_value ParClose
+    ;
+
+check_sat_response
+    : PS_Sat
+    | PS_Unsat
+    | PS_Unknown
+    ;
+
+echo_response
+    : string
+    ;
+
+get_assertions_response
+    : ParOpen term* ParClose
+    ;
+
+get_assignment_response
+    : ParOpen t_valuation_pair* ParClose
+    ;
+
+get_info_response
+    : ParOpen info_response+ ParClose
+    ;
+
+get_model_response
+    : ParOpen model_response* ParClose
+    ;
+
+get_option_response
+    : attribute_value
+    ;
+
+get_proof_response
+    : s_expr
+    ;
+
+get_unsat_assump_response
+    : ParOpen symbol* ParClose
+    ;
+
+get_unsat_core_response
+    : ParOpen symbol* ParClose
+    ;
+
+get_value_response
+    : ParOpen valuation_pair+ ParClose
+    ;
+
+specific_success_response
+    : check_sat_response
+    | echo_response
+    | get_assertions_response
+    | get_assignment_response
+    | get_info_response
+    | get_model_response
+    | get_option_response
+    | get_proof_response
+    | get_unsat_assump_response
+    | get_unsat_core_response
+    | get_value_response
+    ;
+
+general_response
+    : PS_Success
+    | specific_success_response
+    | PS_Unsupported
+    | ParOpen PS_Error string ParClose
+    ;
+
+
+// Parser Rules End
+
+WS  :  [ \t\r\n]+ -> skip
+    ;
diff --git a/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcBackwardXcfaBuilder.java b/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcBackwardXcfaBuilder.java
new file mode 100644
index 0000000000..626d63d471
--- /dev/null
+++ b/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcBackwardXcfaBuilder.java
@@ -0,0 +1,170 @@
+/*
+ *  Copyright 2023 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.frontend.chc;
+
+import hu.bme.mit.theta.chc.frontend.dsl.gen.CHCBaseVisitor;
+import hu.bme.mit.theta.chc.frontend.dsl.gen.CHCParser;
+import hu.bme.mit.theta.core.decl.Decls;
+import hu.bme.mit.theta.core.decl.VarDecl;
+import hu.bme.mit.theta.core.stmt.AssignStmt;
+import hu.bme.mit.theta.core.stmt.AssumeStmt;
+import hu.bme.mit.theta.core.stmt.Stmt;
+import hu.bme.mit.theta.core.type.Expr;
+import hu.bme.mit.theta.core.type.Type;
+import hu.bme.mit.theta.core.type.booltype.BoolLitExpr;
+import hu.bme.mit.theta.core.type.booltype.BoolType;
+import hu.bme.mit.theta.xcfa.model.*;
+import hu.bme.mit.theta.xcfa.passes.ChcPasses;
+import kotlin.Pair;
+import org.antlr.v4.runtime.RuleContext;
+
+import java.util.*;
+
+import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool;
+import static hu.bme.mit.theta.frontend.chc.ChcUtils.*;
+
+public class ChcBackwardXcfaBuilder extends CHCBaseVisitor<Object> implements ChcXcfaBuilder {
+    private final Map<String, XcfaProcedureBuilder> procedures = new HashMap<>();
+    private XcfaBuilder xcfaBuilder;
+    private int callCount = 0;
+
+    @Override
+    public XcfaBuilder buildXcfa(CHCParser parser) {
+        xcfaBuilder = new XcfaBuilder("chc");
+
+        visit(parser.benchmark());
+
+//        xcfaBuilder.addProcess(procBuilder);
+//        xcfaBuilder.setMainProcess(procBuilder);
+        return xcfaBuilder;
+    }
+
+    @Override
+    public Object visitFun_decl(CHCParser.Fun_declContext ctx) {
+        String name = ctx.symbol().getText();
+        if (ctx.symbol().quotedSymbol() != null) name = name.replaceAll("\\|", "");
+        XcfaProcedureBuilder builder = createProcedure(name);
+
+        int i = 0;
+        for (CHCParser.SortContext sort : ctx.sort()) {
+            String varName = name + "_" + i++;
+            Type type = transformSort(sort);
+            builder.addParam(Decls.Var(varName, type), ParamDirection.IN);
+            transformConst(Decls.Const(varName, type), true);
+        }
+
+        procedures.put(name, builder);
+        procedures.put(ctx.symbol().getText(), builder);
+        return super.visitFun_decl(ctx);
+    }
+
+    @Override
+    public Object visitChc_assert(CHCParser.Chc_assertContext ctx) {
+        XcfaProcedureBuilder procedure;
+        if (ctx.chc_tail() != null) {
+            procedure = procedures.get(ctx.chc_head().u_pred_atom().u_predicate().getText());
+            Map<String, VarDecl<?>> vars = createVars(procedure, ctx.var_decl());
+            int i = 0;
+            for (Pair<VarDecl<?>, ParamDirection> param : procedure.getParams()) {
+                if (param.getSecond() != ParamDirection.OUT)
+                    vars.put(ctx.chc_head().u_pred_atom().symbol(i++).getText(), param.getFirst());
+            }
+            XcfaLocation middle = createLocation(procedure);
+            XcfaEdge edge = new XcfaEdge(procedure.getInitLoc(), middle, new SequenceLabel(getTailConditionLabels(ctx.chc_tail(), vars)));
+            procedure.addEdge(edge);
+            createCalls(procedure, middle, procedure.getFinalLoc().get(), ctx.chc_tail().u_pred_atom(), vars);
+        } else {
+            String procName;
+            if (ctx.chc_head() != null) {
+                procName = ctx.chc_head().u_pred_atom().u_predicate().getText();
+            } else {
+                procName = ctx.u_predicate().getText();
+            }
+            procedure = procedures.get(procName);
+            Stmt returnTrue = AssignStmt.create(getOutParam(procedure), BoolLitExpr.of(true));
+            XcfaEdge edge = new XcfaEdge(procedure.getInitLoc(), procedure.getFinalLoc().get(), new StmtLabel(returnTrue, EmptyMetaData.INSTANCE));
+            procedure.addEdge(edge);
+        }
+        return super.visitChc_assert(ctx);
+    }
+
+    @Override
+    public Object visitChc_query(CHCParser.Chc_queryContext ctx) {
+        XcfaProcedureBuilder mainProcedure = createProcedure("query");
+        xcfaBuilder.addEntryPoint(mainProcedure, new ArrayList<>());
+
+        Map<String, VarDecl<?>> vars = createVars(mainProcedure, ctx.var_decl());
+        XcfaLocation middle = createLocation(mainProcedure);
+        XcfaEdge edge = new XcfaEdge(mainProcedure.getInitLoc(), middle, new SequenceLabel(getTailConditionLabels(ctx.chc_tail(), vars)));
+        mainProcedure.addEdge(edge);
+        createCalls(mainProcedure, middle, mainProcedure.getErrorLoc().get(), ctx.chc_tail().u_pred_atom(), vars);
+        return super.visitChc_query(ctx);
+    }
+
+    private int uniqeCounter = 0;
+
+    private XcfaLocation createLocation(XcfaProcedureBuilder builder) {
+        XcfaLocation location = new XcfaLocation("l_" + uniqeCounter++);
+        builder.addLoc(location);
+        return location;
+    }
+
+    private XcfaProcedureBuilder createProcedure(String procName) {
+        XcfaProcedureBuilder builder = new XcfaProcedureBuilder(procName, new ChcPasses());
+        builder.setName(procName);
+        builder.addParam(Decls.Var(procName + "_ret", Bool()), ParamDirection.OUT);
+
+        builder.createInitLoc();
+        builder.createErrorLoc();
+        builder.createFinalLoc();
+
+        xcfaBuilder.addProcedure(builder);
+        return builder;
+    }
+
+    private VarDecl<?> getOutParam(XcfaProcedureBuilder procedure) {
+        Optional<Pair<VarDecl<?>, ParamDirection>> param = procedure.getParams()
+                        .stream().filter(entry -> entry.getSecond() == ParamDirection.OUT).findAny();
+        return param.map(Pair::getFirst).orElse(null);
+    }
+
+    private void createCalls(XcfaProcedureBuilder builder, XcfaLocation start, XcfaLocation end, List<CHCParser.U_pred_atomContext> uPreds, Map<String, VarDecl<?>> localVars) {
+        XcfaLocation from = start;
+        for (CHCParser.U_pred_atomContext uPred : uPreds) {
+            XcfaLocation middle = createLocation(builder);
+            XcfaLocation to = createLocation(builder);
+
+            XcfaProcedureBuilder calledProcedure = procedures.get(uPred.u_predicate().getText());
+            VarDecl<BoolType> ret = Decls.Var(calledProcedure.getName() + "_ret_" + callCount++, Bool());
+            builder.addVar(ret);
+            localVars.put(ret.getName(), ret);
+            List<String> paramNames = new ArrayList<>(uPred.symbol().stream().map(RuleContext::getText).toList());
+            paramNames.add(0, ret.getName());
+            List<? extends Expr<?>> params = paramNames.stream().map(s -> localVars.get(s).getRef()).toList();
+
+            XcfaEdge callEdge = new XcfaEdge(from, middle, new InvokeLabel(calledProcedure.getName(), params, EmptyMetaData.INSTANCE));
+            builder.addEdge(callEdge);
+
+            XcfaEdge assertEdge = new XcfaEdge(middle, to, new StmtLabel(AssumeStmt.of(ret.getRef()), EmptyMetaData.INSTANCE));
+            builder.addEdge(assertEdge);
+
+            from = to;
+        }
+        Stmt returnTrue = AssignStmt.create(getOutParam(builder), BoolLitExpr.of(true));
+        XcfaEdge edge = new XcfaEdge(from, end, new StmtLabel(returnTrue, EmptyMetaData.INSTANCE));
+        builder.addEdge(edge);
+    }
+}
diff --git a/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcForwardXcfaBuilder.java b/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcForwardXcfaBuilder.java
new file mode 100644
index 0000000000..e41eeaf968
--- /dev/null
+++ b/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcForwardXcfaBuilder.java
@@ -0,0 +1,174 @@
+/*
+ *  Copyright 2023 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.frontend.chc;
+
+import hu.bme.mit.theta.chc.frontend.dsl.gen.CHCBaseVisitor;
+import hu.bme.mit.theta.chc.frontend.dsl.gen.CHCParser;
+import hu.bme.mit.theta.core.decl.Decls;
+import hu.bme.mit.theta.core.decl.VarDecl;
+import hu.bme.mit.theta.core.stmt.AssignStmt;
+import hu.bme.mit.theta.core.stmt.HavocStmt;
+import hu.bme.mit.theta.core.type.Type;
+import hu.bme.mit.theta.xcfa.model.*;
+import hu.bme.mit.theta.xcfa.passes.ChcPasses;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+
+import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool;
+import static hu.bme.mit.theta.frontend.chc.ChcUtils.*;
+
+public class ChcForwardXcfaBuilder extends CHCBaseVisitor<Object> implements ChcXcfaBuilder {
+    private XcfaProcedureBuilder builder;
+    private XcfaLocation initLocation;
+    private XcfaLocation errorLocation;
+    private final Map<String, UPred> locations = new HashMap<>();
+
+    @Override
+    public XcfaBuilder buildXcfa(CHCParser parser) {
+        XcfaBuilder xcfaBuilder = new XcfaBuilder("chc");
+        builder = new XcfaProcedureBuilder("main", new ChcPasses());
+        builder.createInitLoc();
+        builder.createErrorLoc();
+        builder.createFinalLoc();
+
+        initLocation = builder.getInitLoc();
+        errorLocation = builder.getErrorLoc().get();
+
+        locations.put(initLocation.getName(), new UPred(initLocation, new ArrayList<>()));
+        locations.put(errorLocation.getName(), new UPred(initLocation, new ArrayList<>()));
+        
+        visit(parser.benchmark());
+
+        xcfaBuilder.addProcedure(builder);
+        xcfaBuilder.addEntryPoint(builder, new ArrayList<>());
+        return xcfaBuilder;
+    }
+
+    @Override
+    public Object visitFun_decl(CHCParser.Fun_declContext ctx) {
+        String name = ctx.symbol().getText();
+        if (ctx.symbol().quotedSymbol() != null) name = name.replaceAll("\\|", "");
+        int i = 0;
+        List<VarDecl<?>> vars = new ArrayList<>();
+        for (CHCParser.SortContext sort : ctx.sort()) {
+            String varName = name + "_" + i++;
+            Type type = transformSort(sort);
+            VarDecl<?> var = Decls.Var(varName, type);
+            vars.add(var);
+            builder.addVar(var);
+            transformConst(Decls.Const(varName, type), true);
+        }
+        XcfaLocation location = new XcfaLocation(name);
+        locations.put(name, new UPred(location, vars));
+        locations.put(ctx.symbol().getText(), new UPred(location, vars));
+        builder.addLoc(location);
+        return super.visitFun_decl(ctx);
+    }
+
+    @Override
+    public Object visitChc_assert(CHCParser.Chc_assertContext ctx) {
+        XcfaLocation from;
+        XcfaLocation to;
+        List<XcfaLabel> labels = new ArrayList<>();
+
+        if (ctx.chc_tail() != null) {
+            from = getTailFrom(ctx.chc_tail());
+            to = getHeadTo(ctx.chc_head());
+            Map<String, VarDecl<?>> vars = createVars(builder, ctx.var_decl());
+            labels.addAll(getIncomingAssignments(ctx.chc_tail(), vars));
+            labels.addAll(getTailConditionLabels(ctx.chc_tail(), vars));
+            labels.addAll(getTargetAssignments(ctx.chc_head(), vars));
+        } else {
+            String locName;
+            if (ctx.chc_head() != null) {
+                locName = ctx.chc_head().u_pred_atom().u_predicate().getText();
+            } else {
+                locName = ctx.u_predicate().getText();
+            }
+            from = initLocation;
+            to = locations.get(locName).location;
+        }
+        XcfaEdge edge = new XcfaEdge(from, to, new SequenceLabel(labels));
+        builder.addEdge(edge);
+        return super.visitChc_assert(ctx);
+    }
+
+    @Override
+    public Object visitChc_query(CHCParser.Chc_queryContext ctx) {
+        XcfaLocation from = getTailFrom(ctx.chc_tail());
+        Map<String, VarDecl<?>> vars = createVars(builder, ctx.var_decl());
+        List<XcfaLabel> labels = new ArrayList<>();
+        labels.addAll(getIncomingAssignments(ctx.chc_tail(), vars));
+        labels.addAll(getTailConditionLabels(ctx.chc_tail(), vars));
+        XcfaEdge edge = new XcfaEdge(from, errorLocation, new SequenceLabel(labels));
+        builder.addEdge(edge);
+        return super.visitChc_query(ctx);
+    }
+
+    private List<XcfaLabel> getIncomingAssignments(CHCParser.Chc_tailContext tail, Map<String, VarDecl<?>> localVars) {
+        List<XcfaLabel> labels = new ArrayList<>();
+        UPred from = locations.get(getTailFrom(tail).getName());
+        tail.u_pred_atom().forEach(u_pred -> {
+            List<? extends VarDecl<?>> params = u_pred.symbol().stream().map(symbol -> localVars.get(symbol.getText())).toList();
+            localVars.values().forEach(var -> { if (!params.contains(var)) labels.add(new StmtLabel(HavocStmt.of(var), EmptyMetaData.INSTANCE)); });
+            labels.addAll(getParamAssignments(params, from.vars));
+        });
+        return labels;
+    }
+
+    private List<XcfaLabel> getTargetAssignments(CHCParser.Chc_headContext head, Map<String, VarDecl<?>> localVars) {
+        List<? extends VarDecl<?>> params = head.u_pred_atom().symbol().stream().map(symbol -> localVars.get(symbol.getText())).toList();
+        UPred to = locations.get(getHeadTo(head).getName());
+        return getParamAssignments(to.vars, params);
+    }
+
+    private XcfaLocation getTailFrom(CHCParser.Chc_tailContext tail) {
+        XcfaLocation from;
+        if (tail.u_pred_atom() != null && !tail.u_pred_atom().isEmpty()) {
+            if (tail.u_pred_atom().size() != 1)
+                throw new UnsupportedOperationException("Non-linear CHCs are not supported with forward transformation, try using the --chc-transformation BACKWARD flag.");
+            from = locations.get(tail.u_pred_atom().get(0).u_predicate().getText()).location;
+        } else {
+            from = initLocation;
+        }
+        return from;
+    }
+
+    private XcfaLocation getHeadTo(CHCParser.Chc_headContext head) {
+        return locations.get(head.u_pred_atom().u_predicate().getText()).location;
+    }
+
+    private List<XcfaLabel> getParamAssignments(List<? extends VarDecl<?>> lhs, List<? extends VarDecl<?>> rhs) {
+        List<XcfaLabel> labels = new ArrayList<>();
+        for (int i = 0; i < lhs.size(); ++i) {
+            labels.add(new StmtLabel(AssignStmt.create(lhs.get(i), rhs.get(i).getRef()), EmptyMetaData.INSTANCE));
+        }
+        return labels;
+    }
+
+    static class UPred {
+        final XcfaLocation location;
+        final List<VarDecl<?>> vars;
+
+        UPred(XcfaLocation location, List<VarDecl<?>> vars) {
+            this.location = location;
+            this.vars = vars;
+        }
+    }
+}
diff --git a/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcFrontend.java b/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcFrontend.java
new file mode 100644
index 0000000000..1cb8c06d4d
--- /dev/null
+++ b/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcFrontend.java
@@ -0,0 +1,47 @@
+/*
+ *  Copyright 2023 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.frontend.chc;
+
+import hu.bme.mit.theta.chc.frontend.dsl.gen.CHCLexer;
+import hu.bme.mit.theta.chc.frontend.dsl.gen.CHCParser;
+import hu.bme.mit.theta.xcfa.model.XCFA;
+import hu.bme.mit.theta.xcfa.model.XcfaBuilder;
+import org.antlr.v4.runtime.CharStream;
+import org.antlr.v4.runtime.CommonTokenStream;
+
+public class ChcFrontend {
+    public enum ChcTransformation {
+        FORWARD,
+        BACKWARD
+    }
+
+    private final ChcTransformation chcTransformation;
+
+    public ChcFrontend(ChcTransformation transformation) {
+        chcTransformation = transformation;
+    }
+
+    public XcfaBuilder buildXcfa(CharStream charStream) {
+        ChcUtils.init(charStream);
+        CHCParser parser = new CHCParser(new CommonTokenStream(new CHCLexer(charStream)));
+        ChcXcfaBuilder chcXcfaBuilder = switch (chcTransformation) {
+            case FORWARD -> new ChcForwardXcfaBuilder();
+            case BACKWARD -> new ChcBackwardXcfaBuilder();
+        };
+        return chcXcfaBuilder.buildXcfa(parser);
+    }
+}
+
diff --git a/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcUtils.java b/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcUtils.java
new file mode 100644
index 0000000000..4eafe9d2e7
--- /dev/null
+++ b/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcUtils.java
@@ -0,0 +1,172 @@
+/*
+ *  Copyright 2023 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.frontend.chc;
+
+import com.google.common.collect.ImmutableList;
+import hu.bme.mit.theta.chc.frontend.dsl.gen.CHCParser;
+import hu.bme.mit.theta.common.Tuple2;
+import hu.bme.mit.theta.core.decl.ConstDecl;
+import hu.bme.mit.theta.core.decl.Decl;
+import hu.bme.mit.theta.core.decl.Decls;
+import hu.bme.mit.theta.core.decl.VarDecl;
+import hu.bme.mit.theta.core.stmt.AssumeStmt;
+import hu.bme.mit.theta.core.type.Expr;
+import hu.bme.mit.theta.core.type.Type;
+import hu.bme.mit.theta.core.type.booltype.BoolType;
+import hu.bme.mit.theta.core.type.bvtype.BvExprs;
+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.GenericSmtLibTermTransformer;
+import hu.bme.mit.theta.solver.smtlib.impl.generic.GenericSmtLibTypeTransformer;
+import hu.bme.mit.theta.solver.smtlib.solver.transformer.SmtLibTermTransformer;
+import hu.bme.mit.theta.solver.smtlib.solver.transformer.SmtLibTypeTransformer;
+import hu.bme.mit.theta.xcfa.model.*;
+import org.antlr.v4.runtime.CharStream;
+import org.antlr.v4.runtime.ParserRuleContext;
+import org.antlr.v4.runtime.misc.Interval;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+
+import static com.google.common.base.Preconditions.checkArgument;
+import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Array;
+import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool;
+import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int;
+import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat;
+import static hu.bme.mit.theta.xcfa.passes.UtilsKt.changeVars;
+
+public class ChcUtils {
+    private static GenericSmtLibSymbolTable initialSymbolTable = new GenericSmtLibSymbolTable();
+    private static GenericSmtLibSymbolTable symbolTable;
+    private static SmtLibTypeTransformer typeTransformer = new GenericSmtLibTypeTransformer(null);
+    private static SmtLibTermTransformer termTransformer = new GenericSmtLibTermTransformer(initialSymbolTable);
+    private static CharStream charStream;
+
+    private ChcUtils() {}
+
+    public static void init(CharStream cs) {
+        initialSymbolTable = new GenericSmtLibSymbolTable();
+        typeTransformer = new GenericSmtLibTypeTransformer(null);
+        termTransformer = new GenericSmtLibTermTransformer(initialSymbolTable);
+        charStream = cs;
+    }
+
+    public static List<XcfaLabel> getTailConditionLabels(CHCParser.Chc_tailContext tail, Map<String, VarDecl<?>> localVars) {
+        List<XcfaLabel> labels = new ArrayList<>();
+        tail.i_formula().forEach(i_formula -> {
+            Expr<BoolType> expr = termTransformer.toExpr(getOriginalText(i_formula), Bool(), null); // null as SmtLibModel, because it is unused
+            List<ConstDecl<?>> exprVars = new ArrayList<>();
+            ExprUtils.collectConstants(expr, exprVars);
+            Map<Decl<?>, VarDecl<?>> varsToLocal = new HashMap<>();
+            for (Decl<?> var : exprVars) {
+                if (localVars.containsKey(var.getName())) {
+                    varsToLocal.put(var, localVars.get(var.getName()));
+                }
+            }
+            Expr<BoolType> replacedExpr = changeVars(expr, varsToLocal);
+            labels.add(new StmtLabel(AssumeStmt.of(replacedExpr), EmptyMetaData.INSTANCE));
+        });
+        return labels;
+    }
+
+    public static String getOriginalText(ParserRuleContext ctx) {
+        return charStream.getText(new Interval(ctx.start.getStartIndex(), ctx.stop.getStopIndex()));
+    }
+
+    public static Map<String, VarDecl<?>> createVars(XcfaProcedureBuilder builder, List<CHCParser.Var_declContext> var_decls) {
+        resetSymbolTable();
+        Map<String, VarDecl<?>> vars = new HashMap<>();
+        for (CHCParser.Var_declContext var_decl : var_decls) {
+            String name = var_decl.symbol().getText();
+            String varName = name + "_" + builder.getEdges().size();
+            Type type = transformSort(var_decl.sort());
+            VarDecl<?> var = Decls.Var(varName, type);
+            builder.addVar(var);
+            transformConst(Decls.Const(name, type), false);
+            vars.put(name, var);
+        }
+        return vars;
+    }
+
+    public static void resetSymbolTable() {
+        symbolTable = new GenericSmtLibSymbolTable(initialSymbolTable);
+        termTransformer = new GenericSmtLibTermTransformer(symbolTable);
+
+    }
+
+    public static Type transformSort(final CHCParser.SortContext ctx) {
+        final String name = ctx.identifier().symbol().getText();
+        switch (name) {
+            case "Int":
+                return Int();
+            case "Bool":
+                return Bool();
+            case "Real":
+                return Rat();
+            case "BitVec":
+                assert ctx.identifier().index().size() == 1;
+                return BvExprs.BvType(Integer.parseInt(ctx.identifier().index().get(0).getText()));
+            case "Array":
+                assert ctx.sort().size() == 2;
+                return Array(transformSort(ctx.sort().get(0)), transformSort(ctx.sort().get(1)));
+            default:
+                throw new UnsupportedOperationException();
+        }
+    }
+
+    public static void transformConst(final ConstDecl<?> decl, boolean initial) {
+        final Type type = decl.getType();
+
+        final Tuple2<List<Type>, Type> extractedTypes = extractTypes(type);
+        final List<Type> paramTypes = extractedTypes.get1();
+        final Type returnType = extractedTypes.get2();
+
+        final String returnSort = typeTransformer.toSort(returnType);
+        final String[] paramSorts = paramTypes.stream().map(typeTransformer::toSort)
+                .toArray(String[]::new);
+
+        final String symbolName = decl.getName();
+        final String symbolDeclaration = String.format(
+                "(declare-fun %s (%s) %s)",
+                symbolName, String.join(" ", paramSorts), returnSort
+        );
+        (initial ? initialSymbolTable : symbolTable).put(decl, symbolName, symbolDeclaration);
+    }
+
+    public static Tuple2<List<Type>, Type> extractTypes(final Type type) {
+        if (type instanceof FuncType<?, ?>) {
+            final FuncType<?, ?> funcType = (FuncType<?, ?>) type;
+
+            final Type paramType = funcType.getParamType();
+            final Type resultType = funcType.getResultType();
+
+            checkArgument(!(paramType instanceof FuncType));
+
+            final Tuple2<List<Type>, Type> subResult = extractTypes(resultType);
+            final List<Type> paramTypes = subResult.get1();
+            final Type newResultType = subResult.get2();
+            final List<Type> newParamTypes = ImmutableList.<Type>builder().add(paramType).addAll(paramTypes).build();
+            final Tuple2<List<Type>, Type> result = Tuple2.of(newParamTypes, newResultType);
+
+            return result;
+        } else {
+            return Tuple2.of(ImmutableList.of(), type);
+        }
+    }
+}
diff --git a/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcXcfaBuilder.java b/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcXcfaBuilder.java
new file mode 100644
index 0000000000..610c401e01
--- /dev/null
+++ b/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcXcfaBuilder.java
@@ -0,0 +1,24 @@
+/*
+ *  Copyright 2023 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.frontend.chc;
+
+import hu.bme.mit.theta.chc.frontend.dsl.gen.CHCParser;
+import hu.bme.mit.theta.xcfa.model.XCFA;
+import hu.bme.mit.theta.xcfa.model.XcfaBuilder;
+
+public interface ChcXcfaBuilder {
+    XcfaBuilder buildXcfa(CHCParser parser);
+}
diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibSymbolTable.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibSymbolTable.java
index d0903ccf00..ec9b7e6add 100644
--- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibSymbolTable.java
+++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibSymbolTable.java
@@ -22,6 +22,13 @@ public GenericSmtLibSymbolTable() {
         constToDeclaration = Maps.synchronizedBiMap(HashBiMap.create());
     }
 
+    public GenericSmtLibSymbolTable(GenericSmtLibSymbolTable table) {
+        constToSymbol = Maps.synchronizedBiMap(HashBiMap.create());
+        constToSymbol.putAll(table.constToSymbol);
+        constToDeclaration = Maps.synchronizedBiMap(HashBiMap.create());
+        constToDeclaration.putAll(table.constToDeclaration);
+    }
+
     @Override
     public boolean definesConst(final ConstDecl<?> constDecl) {
         return constToSymbol.containsKey(constDecl);
diff --git a/subprojects/xcfa/xcfa-cli/build.gradle.kts b/subprojects/xcfa/xcfa-cli/build.gradle.kts
index fce72d2e89..3973a869ab 100644
--- a/subprojects/xcfa/xcfa-cli/build.gradle.kts
+++ b/subprojects/xcfa/xcfa-cli/build.gradle.kts
@@ -5,6 +5,9 @@ plugins {
 
 dependencies {
     implementation(project(":theta-common"))
+    implementation(project(":theta-solver"))
+    implementation(project(":theta-c-frontend"))
+    implementation(project(":theta-chc-frontend"))
     implementation(project(":theta-core"))
     implementation(project(":theta-analysis"))
     implementation(project(":theta-xcfa"))
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt
index 90c7cff4a8..e138b957fc 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt
@@ -33,6 +33,7 @@ import hu.bme.mit.theta.common.logging.Logger
 import hu.bme.mit.theta.common.visualization.Graph
 import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter
 import hu.bme.mit.theta.common.visualization.writer.WebDebuggerLogger
+import hu.bme.mit.theta.frontend.chc.ChcFrontend
 import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig
 import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.BitwiseChecker
 import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager
@@ -44,6 +45,7 @@ import hu.bme.mit.theta.xcfa.cli.utils.XcfaWitnessWriter
 import hu.bme.mit.theta.xcfa.cli.witnesses.XcfaTraceConcretizer
 import hu.bme.mit.theta.xcfa.model.toDot
 import hu.bme.mit.theta.xcfa.passes.LbePass
+import org.antlr.v4.runtime.CharStreams
 import java.io.File
 import java.io.FileInputStream
 import java.io.FileReader
@@ -69,6 +71,12 @@ class XcfaCli(private val args: Array<String>) {
     @Parameter(names = ["--lbe"], description = "Level of LBE (NO_LBE, LBE_LOCAL, LBE_SEQ, LBE_FULL)")
     var lbeLevel: LbePass.LbeLevel = LbePass.LbeLevel.LBE_SEQ
 
+    @Parameter(names = ["--chc"], description = "Parse the input as a Constrained Horn Clause in the CHC-comp format")
+    var chc = false;
+
+    @Parameter(names=["--chc-transformation"], description = "Direction of transformation from CHC to XCFA")
+    var chcTransformation: ChcFrontend.ChcTransformation = ChcFrontend.ChcTransformation.FORWARD;
+
     //////////// backend options ////////////
     @Parameter(names = ["--backend"], description = "Backend analysis to use")
     var backend: Backend = Backend.CEGAR
@@ -172,11 +180,29 @@ class XcfaCli(private val args: Array<String>) {
         if(randomSeed >= 0) XcfaDporLts.random = Random(randomSeed)
 
         val xcfa = try {
-            val stream = FileInputStream(input!!)
-            val xcfaFromC = getXcfaFromC(stream, explicitProperty == ErrorDetection.OVERFLOW)
-            logger.write(Logger.Level.INFO, "Frontend finished: ${xcfaFromC.name}  (in ${swFrontend.elapsed(TimeUnit.MILLISECONDS)} ms)\n")
-            logger.write(Logger.Level.RESULT, "Arithmetic: ${BitwiseChecker.getBitwiseOption()}\n")
-            xcfaFromC
+            if(chc) {
+                var chcFrontend: ChcFrontend
+                val xcfaBuilder = if (chcTransformation == ChcFrontend.ChcTransformation.FORWARD) { // try forward, fallback to backward
+                    chcFrontend = ChcFrontend(chcTransformation)
+                    try {
+                        chcFrontend.buildXcfa(CharStreams.fromStream(FileInputStream(input!!)))
+                    } catch (e: UnsupportedOperationException) {
+                        logger.write(Logger.Level.INFO, "Non-linear CHC found, retrying using backward transformation...")
+                        chcFrontend = ChcFrontend(ChcFrontend.ChcTransformation.BACKWARD)
+                        chcFrontend.buildXcfa(CharStreams.fromStream(FileInputStream(input!!)))
+                    }
+                } else {
+                    chcFrontend = ChcFrontend(chcTransformation)
+                    chcFrontend.buildXcfa(CharStreams.fromStream(FileInputStream(input!!)))
+                }
+                xcfaBuilder.build()
+            } else {
+                val stream = FileInputStream(input!!)
+                val xcfaFromC = getXcfaFromC(stream, explicitProperty == ErrorDetection.OVERFLOW)
+                logger.write(Logger.Level.INFO, "Frontend finished: ${xcfaFromC.name}  (in ${swFrontend.elapsed(TimeUnit.MILLISECONDS)} ms)\n")
+                logger.write(Logger.Level.RESULT, "Arithmetic: ${BitwiseChecker.getBitwiseOption()}\n")
+                xcfaFromC
+            }
         } catch (e: Exception) {
             if (stacktrace) e.printStackTrace();
             logger.write(Logger.Level.RESULT, "Frontend failed!\n")
diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaLabel.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaLabel.kt
index 5453cbe746..08fa0f9ff6 100644
--- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaLabel.kt
+++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaLabel.kt
@@ -32,7 +32,7 @@ sealed class XcfaLabel(open val metadata: MetaData) {
     open fun toStmt(): Stmt = Skip()
 }
 
-data class InvokeLabel(
+data class InvokeLabel @JvmOverloads constructor(
         val name: String,
         val params: List<Expr<*>>,
         override val metadata: MetaData,
diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/FpFunctionsToExprsPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/FpFunctionsToExprsPass.kt
index 17925d4c89..2c90edaef1 100644
--- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/FpFunctionsToExprsPass.kt
+++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/FpFunctionsToExprsPass.kt
@@ -85,7 +85,7 @@ class FpFunctionsToExprsPass : ProcedurePass {
             Preconditions.checkState(expr is RefExpr<*>)
             val assign = Stmts.Assign((expr as RefExpr<*>).decl as VarDecl<FpType>,
                     FpRoundToIntegralExpr.of(FpRoundingMode.RTZ, callStmt.params[1] as Expr<FpType?>))
-            FrontendMetadata.create(assign.expr, "cType", CComplexType.getType(expr))
+            if(FrontendMetadata.getMetadataValue(expr, "cType").isPresent) { FrontendMetadata.create(assign.expr, "cType", CComplexType.getType(expr)) }
             return StmtLabel(assign, metadata = callStmt.metadata)
         }
 
@@ -95,7 +95,7 @@ class FpFunctionsToExprsPass : ProcedurePass {
             Preconditions.checkState(expr is RefExpr<*>)
             val assign = Stmts.Assign((expr as RefExpr<*>).decl as VarDecl<FpType>,
                     FpRoundToIntegralExpr.of(FpRoundingMode.RTP, callStmt.params[1] as Expr<FpType?>))
-            FrontendMetadata.create(assign.expr, "cType", CComplexType.getType(expr))
+            if(FrontendMetadata.getMetadataValue(expr, "cType").isPresent) { FrontendMetadata.create(assign.expr, "cType", CComplexType.getType(expr)) }
             return StmtLabel(assign, metadata = callStmt.metadata)
         }
 
@@ -148,7 +148,7 @@ class FpFunctionsToExprsPass : ProcedurePass {
             val expr = callStmt.params[0]
             Preconditions.checkState(expr is RefExpr<*>)
             val assign = Stmts.Assign((expr as RefExpr<*>).decl as VarDecl<FpType>, FpRoundToIntegralExpr.of(FpRoundingMode.RNA, callStmt.params[1] as Expr<FpType?>))
-            FrontendMetadata.create(assign.expr, "cType", CComplexType.getType(expr))
+            if(FrontendMetadata.getMetadataValue(expr, "cType").isPresent) { FrontendMetadata.create(assign.expr, "cType", CComplexType.getType(expr)) }
             return StmtLabel(assign, metadata = callStmt.metadata)
         }
 
@@ -157,7 +157,7 @@ class FpFunctionsToExprsPass : ProcedurePass {
             val expr = callStmt.params[0]
             Preconditions.checkState(expr is RefExpr<*>)
             val assign = Stmts.Assign((expr as RefExpr<*>).decl as VarDecl<FpType>, FpSqrtExpr.of(FpRoundingMode.RNE, callStmt.params[1] as Expr<FpType?>))
-            FrontendMetadata.create(assign.expr, "cType", CComplexType.getType(expr))
+            if(FrontendMetadata.getMetadataValue(expr, "cType").isPresent) { FrontendMetadata.create(assign.expr, "cType", CComplexType.getType(expr)) }
             return StmtLabel(assign, metadata = callStmt.metadata)
         }
 
@@ -170,7 +170,7 @@ class FpFunctionsToExprsPass : ProcedurePass {
             val expr = callStmt.params[0]
             Preconditions.checkState(expr is RefExpr<*>)
             val assign = Stmts.Assign((expr as RefExpr<*>).decl as VarDecl<FpType>, FpMinExpr.of(callStmt.params[1] as Expr<FpType?>, callStmt.params[2] as Expr<FpType?>))
-            FrontendMetadata.create(assign.expr, "cType", CComplexType.getType(expr))
+            if(FrontendMetadata.getMetadataValue(expr, "cType").isPresent) { FrontendMetadata.create(assign.expr, "cType", CComplexType.getType(expr)) }
             return StmtLabel(assign, metadata = callStmt.metadata)
         }
 
@@ -188,7 +188,7 @@ class FpFunctionsToExprsPass : ProcedurePass {
             val expr = callStmt.params[0]
             Preconditions.checkState(expr is RefExpr<*>)
             val assign = Stmts.Assign((expr as RefExpr<*>).decl as VarDecl<FpType>, FpRoundToIntegralExpr.of(FpRoundingMode.RTN, callStmt.params[1] as Expr<FpType?>))
-            FrontendMetadata.create(assign.expr, "cType", CComplexType.getType(expr))
+            if(FrontendMetadata.getMetadataValue(expr, "cType").isPresent) { FrontendMetadata.create(assign.expr, "cType", CComplexType.getType(expr)) }
             return StmtLabel(assign, metadata = callStmt.metadata)
         }
 
@@ -197,7 +197,7 @@ class FpFunctionsToExprsPass : ProcedurePass {
             val expr = callStmt.params[0]
             Preconditions.checkState(expr is RefExpr<*>)
             val assign = Stmts.Assign((expr as RefExpr<*>).decl as VarDecl<FpType>, FpAbsExpr.of(callStmt.params[1] as Expr<FpType?>))
-            FrontendMetadata.create(assign.expr, "cType", CComplexType.getType(expr))
+            if(FrontendMetadata.getMetadataValue(expr, "cType").isPresent) { FrontendMetadata.create(assign.expr, "cType", CComplexType.getType(expr)) }
             return StmtLabel(assign, metadata = callStmt.metadata)
         }
     }
diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/HavocPromotionAndRange.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/HavocPromotionAndRange.kt
index b239b70f31..fef73cd545 100644
--- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/HavocPromotionAndRange.kt
+++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/HavocPromotionAndRange.kt
@@ -98,7 +98,7 @@ class HavocPromotionAndRange : ProcedurePass {
                 val reversed = list.withIndex().filter { it.value is StmtLabel && (it.value as StmtLabel).stmt is HavocStmt<*> }.reversed()
                 for ((index, value) in reversed) {
                     val varDecl = ((value as StmtLabel).stmt as HavocStmt<*>).varDecl
-                    val type = CComplexType.getType(varDecl.ref)
+                    val type = CComplexType.getType(varDecl.ref) // TODO: what to do when no info is available?
                     if(type !is CVoid) {
                         list.add(index + 1, StmtLabel(type.limit(varDecl.ref), metadata = value.metadata))
                     }
diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt
index 19e5d4ef8e..32dba6e5c2 100644
--- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt
+++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt
@@ -47,4 +47,33 @@ class CPasses(checkOverflow: Boolean) : ProcedurePassManager(listOf(
         UnusedVarPass(),
 ))
 
+class ChcPasses : ProcedurePassManager(/*listOf(
+        // formatting
+        NormalizePass(),
+        DeterministicPass(),
+        // removing redundant elements
+        EmptyEdgeRemovalPass(),
+        UnusedLocRemovalPass(),
+        // optimizing
+        SimplifyExprsPass(),
+        // handling intrinsics
+//        ErrorLocationPass(false),
+//        FinalLocationPass(false),
+//        SvCompIntrinsicsPass(),
+//        FpFunctionsToExprsPass(),
+//        PthreadFunctionsPass(),
+        // trying to inline procedures
+        InlineProceduresPass(),
+        RemoveDeadEnds(),
+        EliminateSelfLoops(),
+        // handling remaining function calls
+//        NondetFunctionPass(),
+        LbePass(),
+        NormalizePass(), // needed after lbe, TODO
+        DeterministicPass(), // needed after lbe, TODO
+//        HavocPromotionAndRange(),
+        // Final cleanup
+        UnusedVarPass(),
+))*/emptyList())
+
 class LitmusPasses : ProcedurePassManager(emptyList())
\ No newline at end of file
diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SimplifyExprsPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SimplifyExprsPass.kt
index 4a40cada0c..0c5d8a1fa9 100644
--- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SimplifyExprsPass.kt
+++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SimplifyExprsPass.kt
@@ -43,7 +43,8 @@ class SimplifyExprsPass : ProcedurePass {
             val newLabels = (edge.label as SequenceLabel).labels.map { if(it is StmtLabel) when(it.stmt) {
                 is AssignStmt<*> -> {
                         val simplified = simplify(it.stmt.expr)
-                        FrontendMetadata.create(simplified, "cType", CComplexType.getType(it.stmt.expr))
+                        if(FrontendMetadata.getMetadataValue(it.stmt.expr, "cType").isPresent)
+                            FrontendMetadata.create(simplified, "cType", CComplexType.getType(it.stmt.expr))
                         StmtLabel(Assign(cast(it.stmt.varDecl, it.stmt.varDecl.type), cast(simplified, it.stmt.varDecl.type)),  metadata = it.metadata)
                     }
                 is AssumeStmt -> {
diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/Utils.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/Utils.kt
index 94f843000c..e63ac3ac15 100644
--- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/Utils.kt
+++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/Utils.kt
@@ -16,6 +16,7 @@
 
 package hu.bme.mit.theta.xcfa.passes
 
+import hu.bme.mit.theta.core.decl.Decl
 import hu.bme.mit.theta.core.decl.VarDecl
 import hu.bme.mit.theta.core.stmt.*
 import hu.bme.mit.theta.core.type.Expr
@@ -77,7 +78,7 @@ fun Stmt.flatten(): List<Stmt> {
     }
 }
 
-fun XcfaLabel.changeVars(varLut: Map<VarDecl<*>, VarDecl<*>>): XcfaLabel =
+fun XcfaLabel.changeVars(varLut: Map<out Decl<*>, VarDecl<*>>): XcfaLabel =
         if(varLut.isNotEmpty())
             when(this) {
                 is InvokeLabel -> InvokeLabel(name, params.map { it.changeVars(varLut) }, metadata = metadata)
@@ -92,7 +93,7 @@ fun XcfaLabel.changeVars(varLut: Map<VarDecl<*>, VarDecl<*>>): XcfaLabel =
             }
         else this
 
-fun Stmt.changeVars(varLut: Map<VarDecl<*>, VarDecl<*>>): Stmt {
+fun Stmt.changeVars(varLut: Map<out Decl<*>, VarDecl<*>>): Stmt {
     val stmt = when (this) {
         is AssignStmt<*> -> AssignStmt.of(cast(varDecl.changeVars(varLut), varDecl.type), cast(expr.changeVars(varLut), varDecl.type))
         is HavocStmt<*> -> HavocStmt.of(varDecl.changeVars(varLut))
@@ -106,8 +107,8 @@ fun Stmt.changeVars(varLut: Map<VarDecl<*>, VarDecl<*>>): Stmt {
     return stmt
 }
 
-fun <T : Type> Expr<T>.changeVars(varLut: Map<VarDecl<*>, VarDecl<*>>): Expr<T> =
-        if (this is RefExpr<T>) (decl as VarDecl<T>).changeVars(varLut).ref
+fun <T : Type> Expr<T>.changeVars(varLut: Map<out Decl<*>, VarDecl<*>>): Expr<T> =
+        if (this is RefExpr<T>) (decl as Decl<T>).changeVars(varLut).ref
         else {
             val ret = this.withOps(this.ops.map { it.changeVars(varLut) })
             if(FrontendMetadata.getMetadataValue(this, "cType").isPresent) {
@@ -116,7 +117,7 @@ fun <T : Type> Expr<T>.changeVars(varLut: Map<VarDecl<*>, VarDecl<*>>): Expr<T>
             ret
         }
 
-fun <T : Type> VarDecl<T>.changeVars(varLut: Map<VarDecl<*>, VarDecl<*>>): VarDecl<T> =
+fun <T : Type> Decl<T>.changeVars(varLut: Map<out Decl<*>, VarDecl<*>>): VarDecl<T> =
         (varLut[this] ?: this) as VarDecl<T>
 
 fun XcfaProcedureBuilder.canInline(): Boolean = canInline(LinkedList())