Commit 9d087704 authored by Mathias Preiner's avatar Mathias Preiner
Browse files

Move benchmarks from pending repository.

parent de0ae893
Pipeline #278 failed with stages
(set-info :smt-lib-version 2.6)
(set-logic UFDTNIA)
(set-info :source |
Generated by: Bernhard Gleiss
Generated on: 2019-3-11
Generator: Rapid
Application: Software Verification
Target solver: Vampire
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "crafted")
(set-info :status unknown)
(declare-datatypes ((Nat 0)) (( (zero) (s (p Nat)) )) )
(declare-sort Time 0)
(declare-sort Trace 0)
(declare-const main_end Time)
(declare-fun l21 (Nat) Time)
(declare-fun l20_rEnd (Nat) Time)
(declare-fun l20_lEnd (Nat) Time)
(declare-fun l20 (Nat) Time)
(declare-fun l18 (Nat) Time)
(declare-fun l15 (Nat) Time)
(declare-fun i (Time Trace) Int)
(declare-fun d (Time Trace) Int)
(declare-fun b (Int Trace) Int)
(declare-fun l22 (Nat) Time)
(declare-fun Sub (Nat Nat) Bool)
(assert (forall ((it Nat)) (Sub it (s it))) )
(assert (forall ((it1 Nat)(it2 Nat)) (=> (Sub it1 it2) (Sub it1 (s it2))) ))
(declare-fun n (Trace) Int)
(declare-const t1 Trace)
(declare-fun l19 (Nat) Time)
(declare-fun l17 (Nat) Time)
(declare-const t2 Trace)
(declare-const l11 Time)
(declare-fun c (Time Trace) Int)
(declare-fun a (Trace) Int)
(declare-const l12 Time)
(declare-fun l25 (Nat) Time)
(declare-fun nl15 (Trace) Nat)
(declare-const l13 Time)
(declare-fun blength (Trace) Int)
(assert
;Semantics of function main
(and
(forall ((tr Trace))
;Update variable c at location l11
(= (c l12 tr) 0)
)
(forall ((tr Trace))
;Update variable d at location l12
(and
(= (d l13 tr) 1)
(= (c l13 tr) (c l12 tr))
)
)
(forall ((tr Trace))
;Update variable i at location l13
(and
(= (i (l15 zero) tr) (blength tr))
(= (c (l15 zero) tr) (c l13 tr))
(= (d (l15 zero) tr) (d l13 tr))
)
)
(forall ((tr Trace))
;Loop at location l15
(and
;Jumping into the body doesn't change the variable values
(forall ((Itl15 Nat))
(and
(= (d (l17 Itl15) tr) (d (l15 Itl15) tr))
(= (c (l17 Itl15) tr) (c (l15 Itl15) tr))
(= (i (l17 Itl15) tr) (i (l15 Itl15) tr))
)
)
;Semantics of the body
(forall ((Itl15 Nat))
(and
;Update variable i at location l17
(and
(= (i (l18 Itl15) tr) (- (i (l17 Itl15) tr) 1))
(= (c (l18 Itl15) tr) (c (l17 Itl15) tr))
(= (d (l18 Itl15) tr) (d (l17 Itl15) tr))
)
;Update variable c at location l18
(and
(= (c (l19 Itl15) tr) (* 2 (c (l18 Itl15) tr)))
(= (d (l19 Itl15) tr) (d (l18 Itl15) tr))
(= (i (l19 Itl15) tr) (i (l18 Itl15) tr))
)
;Update variable d at location l19
(and
(= (d (l20 Itl15) tr) (mod (* (d (l19 Itl15) tr) (d (l19 Itl15) tr)) (n tr)))
(= (c (l20 Itl15) tr) (c (l19 Itl15) tr))
(= (i (l20 Itl15) tr) (i (l19 Itl15) tr))
)
;Semantics of IfElse at location l20
(and
;Jumping into any branch doesn't change the variable values
(and
(= (d (l21 Itl15) tr) (d (l20 Itl15) tr))
(= (c (l21 Itl15) tr) (c (l20 Itl15) tr))
(= (i (l21 Itl15) tr) (i (l20 Itl15) tr))
(= (d (l25 Itl15) tr) (d (l20 Itl15) tr))
(= (c (l25 Itl15) tr) (c (l20 Itl15) tr))
(= (i (l25 Itl15) tr) (i (l20 Itl15) tr))
)
;The branching-condition determines which values to use after the if-statement
(and
(=>
(= (b (i (l20 Itl15) tr) tr) 1)
(= (c (l15 (s Itl15)) tr) (c (l20_lEnd Itl15) tr))
)
(=>
(= (b (i (l20 Itl15) tr) tr) 1)
(= (d (l15 (s Itl15)) tr) (d (l20_lEnd Itl15) tr))
)
(=>
(= (b (i (l20 Itl15) tr) tr) 1)
(= (i (l15 (s Itl15)) tr) (i (l20_lEnd Itl15) tr))
)
(=>
(not
(= (b (i (l20 Itl15) tr) tr) 1)
)
(= (c (l15 (s Itl15)) tr) (c (l20_rEnd Itl15) tr))
)
(=>
(not
(= (b (i (l20 Itl15) tr) tr) 1)
)
(= (d (l15 (s Itl15)) tr) (d (l20_rEnd Itl15) tr))
)
(=>
(not
(= (b (i (l20 Itl15) tr) tr) 1)
)
(= (i (l15 (s Itl15)) tr) (i (l20_rEnd Itl15) tr))
)
)
;Update variable c at location l21
(and
(= (c (l22 Itl15) tr) (+ (c (l21 Itl15) tr) 1))
(= (d (l22 Itl15) tr) (d (l21 Itl15) tr))
(= (i (l22 Itl15) tr) (i (l21 Itl15) tr))
)
;Update variable d at location l22
(and
(= (d (l20_lEnd Itl15) tr) (mod (* (d (l22 Itl15) tr) (a tr)) (n tr)))
(= (c (l20_lEnd Itl15) tr) (c (l22 Itl15) tr))
(= (i (l20_lEnd Itl15) tr) (i (l22 Itl15) tr))
)
;Ignore any skip statement
(= (l25 Itl15) (l20_rEnd Itl15))
)
)
)
;The loop-condition holds always before the last iteration
(forall ((Itl15 Nat))
(=>
(Sub Itl15 (nl15 tr))
(>= (i (l15 Itl15) tr) 0)
)
)
;The loop-condition doesn't hold in the last iteration
(not
(>= (i (l15 (nl15 tr)) tr) 0)
)
;The values after the while-loop are the values from the last iteration
(and
(= (d main_end tr) (d (l15 (nl15 tr)) tr))
(= (c main_end tr) (c (l15 (nl15 tr)) tr))
(= (i main_end tr) (i (l15 (nl15 tr)) tr))
)
)
)
)
)
(assert
(forall ((tr Trace))
;Lemma: Induction on = for var d and location l15
(=>
(forall ((Itl15 Nat))
(=>
(Sub Itl15 (nl15 tr))
(= (d (l15 Itl15) tr) (d (l15 (s Itl15)) tr))
)
)
(= (d (l15 zero) tr) (d (l15 (nl15 tr)) tr))
)
)
)
(assert
(forall ((tr Trace))
;Lemma: Induction on = for var c and location l15
(=>
(forall ((Itl15 Nat))
(=>
(Sub Itl15 (nl15 tr))
(= (c (l15 Itl15) tr) (c (l15 (s Itl15)) tr))
)
)
(= (c (l15 zero) tr) (c (l15 (nl15 tr)) tr))
)
)
)
(assert
(forall ((tr Trace))
;Lemma: Induction on = for var i and location l15
(=>
(forall ((Itl15 Nat))
(=>
(Sub Itl15 (nl15 tr))
(= (i (l15 Itl15) tr) (i (l15 (s Itl15)) tr))
)
)
(= (i (l15 zero) tr) (i (l15 (nl15 tr)) tr))
)
)
)
(assert
(forall ((tr Trace))
;Lemma: if the condition of the loop at l15 holds initially, there is at least one loop iteration
(=>
(>= (i (l15 zero) tr) 0)
(exists ((Itl15 Nat))
(= (s Itl15) (nl15 tr))
)
)
)
)
(assert
(forall ((tr Trace))
;Lemma: Intermediate value for var d at location l15
(forall ((xInt Int)(Itl15 Nat))
(=>
(and
(<= (d (l15 zero) tr) xInt)
(< xInt (d (l15 (nl15 tr)) tr))
(= (d (l15 (s Itl15)) tr) (+ (d (l15 Itl15) tr) 1))
)
(exists ((it Nat))
(and
(= (d (l15 it) tr) xInt)
(Sub it (nl15 tr))
)
)
)
)
)
)
(assert
(forall ((tr Trace))
;Lemma: Intermediate value for var c at location l15
(forall ((xInt Int)(Itl15 Nat))
(=>
(and
(<= (c (l15 zero) tr) xInt)
(< xInt (c (l15 (nl15 tr)) tr))
(= (c (l15 (s Itl15)) tr) (+ (c (l15 Itl15) tr) 1))
)
(exists ((it Nat))
(and
(= (c (l15 it) tr) xInt)
(Sub it (nl15 tr))
)
)
)
)
)
)
(assert
(forall ((tr Trace))
;Lemma: Intermediate value for var i at location l15
(forall ((xInt Int)(Itl15 Nat))
(=>
(and
(<= (i (l15 zero) tr) xInt)
(< xInt (i (l15 (nl15 tr)) tr))
(= (i (l15 (s Itl15)) tr) (+ (i (l15 Itl15) tr) 1))
)
(exists ((it Nat))
(and
(= (i (l15 it) tr) xInt)
(Sub it (nl15 tr))
)
)
)
)
)
)
(assert
(forall ((tr Trace))
;Injectivitiy of Iterators Lemma
(forall ((Itl15 Nat))
(=>
(and
(Sub (s Itl15) (nl15 tr))
(= (d (l15 (s Itl15)) tr) (+ (d (l15 Itl15) tr) 1))
)
(forall ((it1 Nat)(it2 Nat))
(=>
(= (d (l15 it1) tr) (d (l15 it2) tr))
(= it1 it2)
)
)
)
)
)
)
(assert
(forall ((tr Trace))
;Injectivitiy of Iterators Lemma
(forall ((Itl15 Nat))
(=>
(and
(Sub (s Itl15) (nl15 tr))
(= (c (l15 (s Itl15)) tr) (+ (c (l15 Itl15) tr) 1))
)
(forall ((it1 Nat)(it2 Nat))
(=>
(= (c (l15 it1) tr) (c (l15 it2) tr))
(= it1 it2)
)
)
)
)
)
)
(assert
(forall ((tr Trace))
;Injectivitiy of Iterators Lemma
(forall ((Itl15 Nat))
(=>
(and
(Sub (s Itl15) (nl15 tr))
(= (i (l15 (s Itl15)) tr) (+ (i (l15 Itl15) tr) 1))
)
(forall ((it1 Nat)(it2 Nat))
(=>
(= (i (l15 it1) tr) (i (l15 it2) tr))
(= it1 it2)
)
)
)
)
)
)
(assert
;Lemma: Var d at loop l15 has same values on both traces
(=>
(and
(= (d (l15 zero) t1) (d (l15 zero) t2))
(forall ((Itl15 Nat))
(=>
(= (d (l15 Itl15) t1) (d (l15 Itl15) t2))
(= (d (l15 (s Itl15)) t1) (d (l15 (s Itl15)) t2))
)
)
)
(forall ((Itl15 Nat))
(= (d (l15 Itl15) t1) (d (l15 Itl15) t2))
)
)
)
(assert
;Lemma: Var c at loop l15 has same values on both traces
(=>
(and
(= (c (l15 zero) t1) (c (l15 zero) t2))
(forall ((Itl15 Nat))
(=>
(= (c (l15 Itl15) t1) (c (l15 Itl15) t2))
(= (c (l15 (s Itl15)) t1) (c (l15 (s Itl15)) t2))
)
)
)
(forall ((Itl15 Nat))
(= (c (l15 Itl15) t1) (c (l15 Itl15) t2))
)
)
)
(assert
;Lemma: Var i at loop l15 has same values on both traces
(=>
(and
(= (i (l15 zero) t1) (i (l15 zero) t2))
(forall ((Itl15 Nat))
(=>
(= (i (l15 Itl15) t1) (i (l15 Itl15) t2))
(= (i (l15 (s Itl15)) t1) (i (l15 (s Itl15)) t2))
)
)
)
(forall ((Itl15 Nat))
(= (i (l15 Itl15) t1) (i (l15 Itl15) t2))
)
)
)
(assert
;Lemma: If nl15(t2) has same properties as nl15(t1), then nl15(t2)=nl15(t1) (for loop at l15)
(=>
(and
(forall ((Itl15 Nat))
(=>
(Sub Itl15 (nl15 t2))
(>= (i (l15 Itl15) t1) 0)
)
)
(not
(>= (i (l15 (nl15 t2)) t1) 0)
)
)
(= (nl15 t2) (nl15 t1))
)
)
(assert
;Lemma: Equality preservation over traces for var d at location l15
(forall ((itR Nat))
(=>
(and
(= (d (l15 zero) t1) (d (l15 zero) t2))
(forall ((Itl15 Nat))
(=>
(and
(Sub Itl15 itR)
(= (d (l15 Itl15) t1) (d (l15 Itl15) t2))
)
(= (d (l15 (s Itl15)) t1) (d (l15 (s Itl15)) t2))
)
)
)
(= (d (l15 itR) t1) (d (l15 itR) t2))
)
)
)
(assert
;Lemma: Equality preservation over traces for var c at location l15
(forall ((itR Nat))
(=>
(and
(= (c (l15 zero) t1) (c (l15 zero) t2))
(forall ((Itl15 Nat))
(=>
(and
(Sub Itl15 itR)
(= (c (l15 Itl15) t1) (c (l15 Itl15) t2))
)
(= (c (l15 (s Itl15)) t1) (c (l15 (s Itl15)) t2))
)
)
)
(= (c (l15 itR) t1) (c (l15 itR) t2))
)
)
)
(assert
;Lemma: Equality preservation over traces for var i at location l15
(forall ((itR Nat))
(=>
(and
(= (i (l15 zero) t1) (i (l15 zero) t2))
(forall ((Itl15 Nat))
(=>
(and
(Sub Itl15 itR)
(= (i (l15 Itl15) t1) (i (l15 Itl15) t2))
)
(= (i (l15 (s Itl15)) t1) (i (l15 (s Itl15)) t2))
)
)
)
(= (i (l15 itR) t1) (i (l15 itR) t2))
)
)
)
(assert
;Lemma: Equality preservation over traces for var d at location l15
(forall ((itL Nat))
(=>
(and
(= (d (l15 itL) t1) (d (l15 itL) t2))
(forall ((Itl15 Nat))
(=>
(and
(Sub itL (s Itl15))
(Sub Itl15 (nl15 t1))
(= (d (l15 Itl15) t1) (d (l15 Itl15) t2))
)
(= (d (l15 (s Itl15)) t1) (d (l15 (s Itl15)) t2))
)
)
(= (l15 (nl15 t1)) (l15 (nl15 t2)))
)
(= (d (l15 (nl15 t1)) t1) (d (l15 (nl15 t1)) t2))
)
)
)
(assert
;Lemma: Equality preservation over traces for var c at location l15
(forall ((itL Nat))
(=>
(and
(= (c (l15 itL) t1) (c (l15 itL) t2))
(forall ((Itl15 Nat))
(=>
(and
(Sub itL (s Itl15))
(Sub Itl15 (nl15 t1))
(= (c (l15 Itl15) t1) (c (l15 Itl15) t2))
)
(= (c (l15 (s Itl15)) t1) (c (l15 (s Itl15)) t2))
)
)
(= (l15 (nl15 t1)) (l15 (nl15 t2)))
)
(= (c (l15 (nl15 t1)) t1) (c (l15 (nl15 t1)) t2))
)
)
)
(assert
;Lemma: Equality preservation over traces for var i at location l15
(forall ((itL Nat))
(=>
(and
(= (i (l15 itL) t1) (i (l15 itL) t2))
(forall ((Itl15 Nat))
(=>
(and
(Sub itL (s Itl15))
(Sub Itl15 (nl15 t1))
(= (i (l15 Itl15) t1) (i (l15 Itl15) t2))
)
(= (i (l15 (s Itl15)) t1) (i (l15 (s Itl15)) t2))
)
)
(= (l15 (nl15 t1)) (l15 (nl15 t2)))
)
(= (i (l15 (nl15 t1)) t1) (i (l15 (nl15 t1)) t2))
)
)
)
(assert
;Lemma: Synchronization of orderings for var d at location l15
(forall ((tr Trace)(it1 Nat)(it2 Nat))
(=>
(and
(Sub it1 it2)
(= (d (l15 zero) t1) (d (l15 zero) t2))
(forall ((tr3 Trace)(Itl15 Nat))
(= (d (l15 (s Itl15)) tr3) (+ (d (l15 Itl15) tr3) 1))
)
)
(< (d (l15 it1) tr) (d (l15 it2) tr))
)
)
)
(assert
;Lemma: Synchronization of orderings for var c at location l15
(forall ((tr Trace)(it1 Nat)(it2 Nat))
(=>
(and
(Sub it1 it2)
(= (c (l15 zero) t1) (c (l15 zero) t2))
(forall ((tr3 Trace)(Itl15 Nat))
(= (c (l15 (s Itl15)) tr3) (+ (c (l15 Itl15) tr3) 1))
)
)
(< (c (l15 it1) tr) (c (l15 it2) tr))
)
)
)
(assert
;Lemma: Synchronization of orderings for var i at location l15
(forall ((tr Trace)(it1 Nat)(it2 Nat))
(=>
(and
(Sub it1 it2)
(= (i (l15 zero) t1) (i (l15 zero) t2))
(forall ((tr3 Trace)(Itl15 Nat))
(= (i (l15 (s Itl15)) tr3) (+ (i (l15 Itl15) tr3) 1))
)
)
(< (i (l15 it1) tr) (i (l15 it2) tr))
)
)
)
(assert
;Theory axiom: forall x y z. (x + y) + z) = (x + z) + y
(forall ((xInt Int)(yInt Int)(zInt Int))
(= (+ (+ xInt yInt) zInt) (+ (+ xInt zInt) yInt))
)
)
; negated conjecture
(assert
(not