src/HOL/SMT/Examples/cert/z3_bv_arith_06
changeset 33006 39f73a59e855
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SMT/Examples/cert/z3_bv_arith_06	Tue Oct 20 10:11:30 2009 +0200
     1.3 @@ -0,0 +1,4 @@
     1.4 +(benchmark Isabelle
     1.5 +:assumption (not (= (bvsub bv11[8] bv27[8]) (bvneg bv16[8])))
     1.6 +:formula true
     1.7 +)