# [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.*