--- a/src/HOL/SMT/Examples/cert/z3_bv_01 Tue Feb 02 18:11:21 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-(benchmark Isabelle
-:extrafuns (
- (uf_1 BitVec[2] Int)
- )
-:assumption (= (uf_1 bv0[2]) 0)
-:assumption (= (uf_1 bv1[2]) 1)
-:assumption (= (uf_1 bv2[2]) 2)
-:assumption (= (uf_1 bv3[2]) 3)
-:assumption (forall (?x1 BitVec[2]) (< 0 (uf_1 ?x1)))
-:assumption (not (forall (?x2 Int) (implies (< ?x2 0) (forall (?x3 BitVec[2]) (< ?x2 (uf_1 ?x3))))))
-:formula true
-)