From 8c24db1994be20528fd0285844ee6a32b847d2aa Mon Sep 17 00:00:00 2001 From: rustanleino Date: Thu, 6 Aug 2009 00:53:19 +0000 Subject: Removed a temporary file that is created by the test script. --- Test/inline/expansion2.sx | 178 ---------------------------------------------- 1 file changed, 178 deletions(-) delete mode 100644 Test/inline/expansion2.sx (limited to 'Test/inline') diff --git a/Test/inline/expansion2.sx b/Test/inline/expansion2.sx deleted file mode 100644 index 7417aab2..00000000 --- a/Test/inline/expansion2.sx +++ /dev/null @@ -1,178 +0,0 @@ -; Boogie program verifier version 2.00, Copyright (c) 2003-2009, Microsoft. -; Command Line Options: -nologo -logPrefix:inline /proverLog:expansion2.sx expansion2.bpl -; Proof obligation: foo -; Z3 command line: c:\Program Files\Microsoft Research\Z3-2.0\bin\z3.exe /si /@ /cex:5 /t:0 -; User supplied Z3 options: -; Prover options: -; -(SETPARAMETER MODEL_PARTIAL true) -(SETPARAMETER MODEL_VALUE_COMPLETION false) -(SETPARAMETER MODEL_HIDE_UNUSED_PARTITIONS false) -(SETPARAMETER MODEL_V1 true) -(SETPARAMETER ASYNC_COMMANDS false) -(SETPARAMETER PHASE_SELECTION 0) -(SETPARAMETER RESTART_STRATEGY 0) -(SETPARAMETER RESTART_FACTOR |1.5|) -(SETPARAMETER NNF_SK_HACK true) -(SETPARAMETER QI_EAGER_THRESHOLD 100) -(SETPARAMETER ARITH_RANDOM_INITIAL_VALUE true) -(SETPARAMETER SORT_AND_OR false) -(SETPARAMETER CASE_SPLIT 3) -(SETPARAMETER DELAY_UNITS true) -(SETPARAMETER DELAY_UNITS_THRESHOLD 16) -(SETPARAMETER TYPE_CHECK true) -(SETPARAMETER BV_REFLECT true) -; ------------------------------------------------------------------------- -; Boogie 2 universal background predicate for Z3 (Simplify notation with types) -; Copyright (c) 2004-2009, Microsoft Corp. - -(DEFTYPE $int :BUILTIN Int) -(DEFTYPE $bool :BUILTIN bool) -(DEFTYPE U) -(DEFTYPE T) - -(DEFOP <: U U $bool) ; used for translation with type premisses -(DEFOP <:: T U U $bool) ; used for translation with type arguments - -(BG_PUSH (AND - - ; false is not true - - (DISTINCT |@false| |@true|) - - ; we assume type correctness of the operations here - ; a-l>=0 ==> (v ++ w:l)[a:b] = v[a-l:b-l] - (FORALL (v lv w lw lvw a b) - (QID bv:e:c1) - (PATS ($bv_extract ($bv_concat v lv w lw) lvw a b)) - (IMPLIES - (>= (- a lw) 0) - (EQ ($bv_extract ($bv_concat v lv w lw) lvw a b) ($bv_extract v lv (- a lw) (- b lw))))) - - ; b<=l ==> (v ++ w:l)[a:b] = w[a:b] - (FORALL (v lv w lw lvw a b) - (QID bv:e:c2) - (PATS ($bv_extract ($bv_concat v lv w lw) lvw a b)) - (IMPLIES - (<= b lw) - (EQ ($bv_extract ($bv_concat v lv w lw) lvw a b) ($bv_extract w lw a b)))) - - ; v:l - ; a>=x || b<=y ==> (v[x:l] ++ w ++ v[0:y])[a:b] = v[a:b] - (FORALL (v lv x lxv w lw lwy y a b) - (QID bv:e:c3) - (PATS - ($bv_extract - ($bv_concat - ($bv_extract v lv x lv) lxv - ($bv_concat - w lw - ($bv_extract v lv 0 y) y) lwy) lv a b)) - (IMPLIES - (AND - (EQ lw (- x y)) - (EQ lxv (- lv x)) - (EQ lwy (+ w y)) - (OR (>= a x) (<= b y))) - (EQ - ($bv_extract - ($bv_concat - ($bv_extract v lv x lv) lxv - ($bv_concat - w lw - ($bv_extract v lv 0 y) y) lwy) lv a b) - ($bv_extract v lv a b)))) - - ; a>=x ==> (v[x:l] ++ w)[a:b] = v[a:b] - (FORALL (v lv x lxv w a b) - (QID bv:e:c4) - (PATS - ($bv_extract - ($bv_concat - ($bv_extract v lv x lv) lxv - w x) - lv a b)) - (IMPLIES - (AND - (EQ lxv (- lv x)) - (>= a x)) - (EQ - ($bv_extract - ($bv_concat - ($bv_extract v lv x lv) lxv - w x) - lv a b) - ($bv_extract v lv a b)))) - - (FORALL (v l) - (QID bv:e:0) - (PATS ($bv_extract v l 0 l)) - (EQ ($bv_extract v l 0 l) v)) - - (FORALL (n) - (QID bv:pow) - (PATS ($pow2 n)) - (IMPLIES (> n 0) (EQ ($pow2 n) (* 2 ($pow2 (- n 1)))))) - - (EQ ($pow2 0) 1) - - ; 0 <= v < 2^Y ==> 0bvX ++ v[0:Y] == v - (FORALL (v l a b) - (QID bv:e:pow) - (PATS ($bv_concat 0 b ($bv_extract v l 0 a) a)) - (IMPLIES - (AND - (<= 0 v) - (< v ($pow2 a)) - (EQ l (+ a b))) - (EQ ($bv_concat 0 b ($bv_extract v l 0 a) a) v))) - - ; X > 0 ==> 0bvX ++ v >= 0 - (FORALL (v a b) - (QID bv:e:pos) - (PATS ($bv_concat 0 b v a)) - (IMPLIES - (> b 0) - (>= ($bv_concat 0 b v a) 0))) - - ;; unsound? -; (FORALL (lv w lw) -; (QID bv:c:0) -; (PATS ($bv_concat 0 lv w lw)) -; (EQ ($bv_concat 0 lv w lw) w)) - ;; matching loop -; (FORALL (v l1 a b l2 c d) -; (QID bv:e:e) -; (PATS ($bv_extract ($bv_extract v l1 a b) l2 c d)) -; (EQ ($bv_extract ($bv_extract v l1 a b) l2 c d) ($bv_extract v l1 (+ c a) (+ d a)))) - - - ; Reflect plus - (FORALL (a b) (PATS (Reflect$Add a b)) (EQ (Reflect$Add a b) (+ a b))) - -)) ;; AND, BG_PUSH -; End Boogie universal background predicate -; ------------------------------------------------------------------------- - - - -(DEFOP Ctor T $int) -(DEFOP intType T) -(DEFOP boolType T) -(DEFOP int_2_U $int U) -(DEFOP U_2_int U $int) -(DEFOP type U T) -(DEFOP bool_2_U $bool U) -(DEFOP U_2_bool U $bool) -(BG_PUSH -(AND (EQ (Ctor (intType)) 0) (EQ (Ctor (boolType)) 1) (FORALL (arg0 :TYPE $int) (PATS (int_2_U arg0)) (QID typeInv:U_2_int) (EQ (U_2_int (int_2_U arg0)) arg0)) (FORALL (x :TYPE U) (PATS (int_2_U (U_2_int x))) (QID cast:U_2_int) (IMPLIES (EQ (type x) (intType)) (EQ (int_2_U (U_2_int x)) x))) (FORALL (arg0@@0 :TYPE $int) (PATS (int_2_U arg0@@0)) (QID funType:int_2_U) (EQ (type (int_2_U arg0@@0)) (intType))) (FORALL (arg0@@1 :TYPE $bool) (PATS (bool_2_U arg0@@1)) (QID typeInv:U_2_bool) (IFF (U_2_bool (bool_2_U arg0@@1)) arg0@@1)) (FORALL (x@@0 :TYPE U) (PATS (bool_2_U (U_2_bool x@@0))) (QID cast:U_2_bool) (IMPLIES (EQ (type x@@0) (boolType)) (EQ (bool_2_U (U_2_bool x@@0)) x@@0))) (FORALL (arg0@@2 :TYPE $bool) (PATS (bool_2_U arg0@@2)) (QID funType:bool_2_U) (EQ (type (bool_2_U arg0@@2)) (boolType)))) -) -(BG_PUSH -(AND (FORALL (x@@1 :TYPE U) (NOPATS (U_2_int x@@1) (U_2_bool x@@1)) (QID bg:subtype-refl) (<: x@@1 x@@1)) (FORALL (x@@2 :TYPE U y :TYPE U z :TYPE U) (PATS (MPAT (<: x@@2 y) (<: y z))) (QID bg:subtype-trans) (LET ((TERM alpha (type x@@2))) (IMPLIES (AND (EQ (type y) alpha) (EQ (type z) alpha)) (IMPLIES (AND (<: x@@2 y) (<: y z)) (<: x@@2 z))))) (FORALL (x@@3 :TYPE U y@@0 :TYPE U) (PATS (MPAT (<: x@@3 y@@0) (<: y@@0 x@@3))) (QID bg:subtype-antisymm) (LET ((TERM alpha@@0 (type x@@3))) (IMPLIES (EQ (type y@@0) alpha@@0) (IMPLIES (AND (<: x@@3 y@@0) (<: y@@0 x@@3)) (EQ x@@3 y@@0))))) (FORALL (z@@0 :TYPE $int) (QID expansio.6:15) (SKOLEMID 2) (IMPLIES (> z@@0 12) (> z@@0 0))) (FORALL (y@@1 :TYPE $int) (QID expansio.7:15) (SKOLEMID 3) (IMPLIES (> (+ y@@1 1) 1) (> y@@1 0)))) -) -; Initialized all axioms. -(BG_PUSH -TRUE -) -(LET ((FORMULA anon0_correct (IMPLIES (LBLPOS |+107| TRUE) (IMPLIES TRUE (AND (LBLNEG |@164| (> 12 0)) (IMPLIES (> 12 0) (AND (LBLNEG |@168| (EQ (+ 3 1) 4)) (IMPLIES (EQ (+ 3 1) 4) (IMPLIES TRUE TRUE))))))))) anon0_correct) -; Valid -- cgit v1.2.3