# HG changeset patch # User boehmes # Date 1398978247 -7200 # Node ID ad1bbed53788d1fd6451bb8d7a73dc0bea740f73 # Parent 689a3eeb6f9e63bc8d981e3907f54fa6d0beffe6 disable bad Z3 proof diff -r 689a3eeb6f9e -r ad1bbed53788 src/HOL/SMT_Examples/SMT_Tests.thy --- a/src/HOL/SMT_Examples/SMT_Tests.thy Thu May 01 22:57:38 2014 +0200 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy Thu May 01 23:04:07 2014 +0200 @@ -731,7 +731,7 @@ "p = \ cx = 3, cy = 4, black = True \ \ p \ black := True \ \ cx := 3 \ \ cy := 4 \ = p" using point.simps bw_point.simps - by smt2+ + by smt+ (* FIXME: bad Z3-4.3.x proof with smt2 *) lemma "\ cx = 3, cy = 4, black = b \ \ black := w \ = \ cx = 3, cy = 4, black = w \"