## Smt-lib2 counterexample syntax extension

Dear Why3 dev team,

We propose an extension of the smt-lib2 model format that can handle both assertions and declaration of constants. Our proposition is to use the *new* keywords declare-const and assert to declare fresh constants and to express assertions, respectively.

```
(declare-const <name> <type>)
(assert <expression>)
```

The main motivation for our request is to adapt the smt-lib2 format to the (richer) counterexamples (CE) produced by our SMT solver Alt-Ergo (AE).

We recently instrumented AE to produce CE in the smt-lib2 format. However, AE can output models implying intervals (like `x in [0;100]`

) or linear constraints (like `x = y + 1`

) that cannot be expressed in the (too restricted) format of smt-lib2 . Now, by combining assert, declare-const, AE could produce models for such CE .

For instance, to express that a variable x is in the interval [0;100], AE could output the following model:

```
(declare-const c_x Int)
(assert (and (<= c_x 100) (>= c_x 0)))
(define-fun x () Int c_x)
```

or even simpler:

```
(declare-const x Int)
(assert (and (< x 100) (> x 0)))
```

Our proposition could also be very useful to output expressive models for other datatypes.
For instance, suppose a CE contains a record x with two labels `a`

and `b`

of type Int, and that `x.a in [0;100]`

and `x.b = 42`

. Such a model could be expressed as follows:

```
(declare-datatype t (mk (a Int) (b Int)))
(declare-const c_a Int)
(assert (and (< c_a 100)(>= c_a 0)))
(define-fun x () t (mk c_a 42))
```

As another example, suppose a CE contains an enumeration datatype `type u = A | B | C | D`

and a variable i of type u which is known to be only A or B.
Such a model could be expressed as follows:

```
(declare-datatype u (A B C D))
(declare-const c_i u)
(assert (or (= c_i A) (= c_i B)))
(define-fun i () u c_i)
```

Best regards,

Alt-Ergo dev. team