# [isabelle] ON Isabelle/SMT counter_example

```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.