# Re: [isabelle] ON Isabelle/SMT counter_example

```Hi,

```
The short answer: Counterexamples produced by SMT solvers might often by spurious, and the corresponding code in Isabelle/HOL is not well tested and currently experimental. You might instead consider Nitpick or Quickcheck for producing counterexamples.
```

```
The SMT interface in Isabelle/HOL applies transformations before giving a formula to the SMT solver. These transformations are tuned for proving a goal, but might unfortunately lead to strange counterexamples.
```
```
One particular transformation encodes any formula of type bool that is not a Boolean constant nor a Boolean connective into an equation with the constant term_true. The idea is to turn atomic formulas into terms (in the sense of first-order logic). These terms get a new type, called term_bool, to distinguish them from formulas. For the SMT solver, the constant term_true belongs to the type term_bool.
```

P --> Q

is transformed into

(P = term_true) --> (Q = term_true)

```
where P and Q are now of type term_bool. In addition, the SMT solver gets the fact
```
term_true ~= term_false

```
Hence, it will know that there are at least two distinct values of type term_bool. For the SMT solver, however, there might also be other values of type term_bool. This is because, for technical reasons, the SMT solver does not get an exhaustion rule such as
```
ALL x::term_bool. x = term_true | x = term_false

```
Therefore, an SMT counterexample produced for your goal might refer to further values of type term_bool. And indeed, this is what happens:
```
```
```SMT: Result:
f2 -> S1!val!1
f1 -> S1!val!0
f3 -> S1!val!0
f4 -> S1!val!2
sat
```
```
```
The names f1 and f2 abbreviate term_true and term_false, whereas f3 and f4 abbreviate P and Q. The value "S1!val!1" is what Z3 assigns to term_false. The above output can thus be read as follows: For P = term_true and Q having some other value, your goal does not hold.
```
```
Now, there is some piece of code in Isabelle's SMT integration that parses the above output and tries to turn it into a better readable form. It produces:
```
```
```SMT: Solver z3: Counterexample found (possibly spurious):
P = ??.SMT.term_true
```
```
```
As you already noted, a value for Q is missing. This is just one indication that currently the parsing code for counterexamples is just experimental and not well tested. You can look at it in your Isabelle distribution at src/HOL/Tools/SMT/z3_model.ML. In case, you desperately need counterexamples from Z3 (or some other SMT solver) instead of relying on Nitpick or Quickcheck, you are invited to extend and modify this code. I suggest to discuss the details privately (not on this list).
```
Cheers,
Sascha

Quoting li yongjian <lyj238 at gmail.com>:

```
```Hi:
. I have two questions on Isabelle/SMT.

1) is the intermedia formula which is tranformed from HOL formula, and
will be fed
into z3.
2) is the counterexample format after z3 checked the formula has

I use the following as a running example.

lemma "P --> Q" using [[smt_trace]] by smt;

by my understanding,

The intermediate formula should be a propostion logical formula in SMT
format for
"~(p-->q)"

The counter-ex should say an assignment: P: true; and
Q:Flase.

but I'm confued about the Isabelle's trace output. Can anyone explain,
(see Isabelle's output below):

Does the terms f1 f2 make sense?

The assignment only says P = ??.SMT.term_true, but this is not complete,
Q is False is also needed to specify?

regards!

f1 = ??.SMT.term_true
f2 = ??.SMT.term_false

The counterexample output is just as follows:
SMT: Assertions:
\<not> (P \<longrightarrow> Q)

SMT: Names:
sorts:
S1 = bool
functions:
f1 = ??.SMT.term_true
f2 = ??.SMT.term_false
f3 = P
f4 = Q

SMT: Problem:
(benchmark Isabelle
:status unknown
:logic AUFLIA
:extrasorts ( S1)
:extrafuns (
(f1 S1)
(f2 S1)
(f3 S1)
(f4 S1)
)
:assumption (not (= f1 f2))
:assumption (not (implies (= f3 f1) (= f4 f1)))
:formula true)
; solver: z3
; timeout: 20.0
; random seed: 1
; arguments:
; DISPLAY_PROOF=true
; PROOF_MODE=2
; -rs:1
; MODEL=true
; -smt

SMT: Invoking SMT solver "z3" ...

SMT: Solver:

SMT: Result:
f2 -> S1!val!1
f1 -> S1!val!0
f3 -> S1!val!0
f4 -> S1!val!2
sat

SMT: Solver z3: Counterexample found (possibly spurious):
P = ??.SMT.term_true

```
```

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.