src/HOL/SMT_Examples/SMT_Tests.thy

 
 theory SMT_Tests
 imports Complex_Main
 begin
 
-smt_status
 smt2_status
 
 text {* Most examples are taken from various Isabelle theories and from HOL4. *}
 
 

   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
      p \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> = p"
   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
      p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p"
   using point.simps bw_point.simps
-  by smt+ (* smt2 FIXME: bad Z3 4.3.x proof *)
+  sorry (* smt2 FIXME: bad Z3 4.3.x proof *)
 
 lemma
   "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>"
   "\<lparr> cx = 3, cy = 4, black = True \<rparr> \<lparr> black := False \<rparr> =
      \<lparr> cx = 3, cy = 4, black = False \<rparr>"