(Revision: Mar 7, 2018)

Comments on this document can be submitted through Gitter or emailed directly to the organizers.

The format used for the CHC-COMP benchmarks is based on the SMT-LIB language version 2.6. Specifically, the format is a syntactic fragment of SMT-LIB format with the restrictions outlined in the rest of this document.

```
benchmark ::=
logic
fun_decl+
(assert chc_assert)*
(assert chc_query)
(check-sat)
logic ::= (set-logic HORN)
fun_decl ::= (declare-fun symbol ( sort* ) Bool)
chc_assert ::= ;; a well-formed first-order sentence of the form
| (forall ( var_decl+ ) (=> chc_tail chc_head))
| chc_head
var_decl ::= (symbol sort)
chc_head ::=
| (u_predicate var*) , where all variables are DISTINCT
chc_tail ::=
| (u_predicate var*)
| i_formula
| (and (u_predicate var*)+ i_formula*)
chc_query ::= ;; a well-formed first-order sentence of the form
| (forall ( var_decl+ ) (=> chc_tail false)
u_predicate ::= uninterperted predicate (i.e., Boolean function)
i_formula ::=
an SMT-LIB formula over variables, and interpreted functions and predicates
```

An example of an input in the CHC-COMP format is shown below:

```
(set-logic HORN)
(set-info :status sat)
(declare-fun Inv (Int) Bool)
;; fact
(assert (forall ((x Int)) (=> (= x 0) (Inv x))))
;; chc
(assert (forall ((x Int) (y Int))
(=> (and (Inv x) (<= x 10) (= y (+ x 1)))
(Inv y))))
;; query
(assert (forall ((x Int)) (=> (and (Inv x) (> x 15)) false)))
(check-sat)
```