Skip to content

Commit

Permalink
update golds
Browse files Browse the repository at this point in the history
  • Loading branch information
@LeventErkok
LeventErkok committed Sep 16, 2024
1 parent 32f041f commit 0d06440
Show file tree
Hide file tree
Showing 7 changed files with 105 additions and 182 deletions.
36 changes: 8 additions & 28 deletions SBVTestSuite/GoldFiles/constArr2_SArray.gold
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,9 @@
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-option :pp.max_depth 4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (set-option :model.inline_def true )
[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
Expand All @@ -14,24 +17,12 @@
[GOOD] (define-fun s5 () Int 2)
[GOOD] (define-fun s7 () Int 3)
[GOOD] (define-fun s9 () Int 75)
[GOOD] (define-fun s14 () Int 12)
[GOOD] (define-fun s15 () Int 5)
[GOOD] (define-fun s16 () Int 6)
[GOOD] (define-fun s14 () (Array Int Int) (store (store (store (store ((as const (Array Int Int)) 2) 75 5) 3 6) 2 5) 1 12))
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () Int) ; tracks user variable "i"
[GOOD] (declare-fun s1 () Int) ; tracks user variable "j"
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- arrays ---
[GOOD] (define-fun array_0 () (Array Int Int) ((as const (Array Int Int)) 2))
[GOOD] (declare-fun array_1 () (Array Int Int))
[GOOD] (define-fun array_1_initializer_0 () Bool (= array_1 (store array_0 s3 s14)))
[GOOD] (declare-fun array_2 () (Array Int Int))
[GOOD] (define-fun array_2_initializer_0 () Bool (= array_2 (store array_1 s5 s15)))
[GOOD] (declare-fun array_3 () (Array Int Int))
[GOOD] (define-fun array_3_initializer_0 () Bool (= array_3 (store array_2 s7 s16)))
[GOOD] (declare-fun array_4 () (Array Int Int))
[GOOD] (define-fun array_4_initializer_0 () Bool (= array_4 (store array_3 s9 s15)))
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
Expand All @@ -43,25 +34,14 @@
[GOOD] (define-fun s11 () Bool (or s8 s10))
[GOOD] (define-fun s12 () Bool (or s6 s11))
[GOOD] (define-fun s13 () Bool (or s4 s12))
[GOOD] (define-fun s17 () Int (select array_4 s0))
[GOOD] (define-fun s18 () Int (select array_4 s1))
[GOOD] (define-fun s19 () Bool (= s17 s18))
[GOOD] ; --- arrayDelayeds ---
[GOOD] ; --- arraySetups ---
[GOOD] (define-fun array_0_initializer () Bool true) ; no initialization needed
[GOOD] (define-fun array_1_initializer () Bool array_1_initializer_0)
[GOOD] (assert array_1_initializer)
[GOOD] (define-fun array_2_initializer () Bool array_2_initializer_0)
[GOOD] (assert array_2_initializer)
[GOOD] (define-fun array_3_initializer () Bool array_3_initializer_0)
[GOOD] (assert array_3_initializer)
[GOOD] (define-fun array_4_initializer () Bool array_4_initializer_0)
[GOOD] (assert array_4_initializer)
[GOOD] (define-fun s15 () Int (select s14 s0))
[GOOD] (define-fun s16 () Int (select s14 s1))
[GOOD] (define-fun s17 () Bool (= s15 s16))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert s2)
[GOOD] (assert s13)
[GOOD] (assert s19)
[GOOD] (assert s17)
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
Expand Down
37 changes: 8 additions & 29 deletions SBVTestSuite/GoldFiles/constArr_SArray.gold
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,9 @@
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-option :pp.max_depth 4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (set-option :model.inline_def true )
[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
Expand All @@ -14,25 +17,12 @@
[GOOD] (define-fun s5 () Int 2)
[GOOD] (define-fun s7 () Int 3)
[GOOD] (define-fun s9 () Int 75)
[GOOD] (define-fun s14 () Int 7)
[GOOD] (define-fun s15 () Int 12)
[GOOD] (define-fun s16 () Int 5)
[GOOD] (define-fun s17 () Int 6)
[GOOD] (define-fun s14 () (Array Int Int) (store (store (store (store ((as const (Array Int Int)) 7) 75 5) 3 6) 2 5) 1 12))
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () Int) ; tracks user variable "i"
[GOOD] (declare-fun s1 () Int) ; tracks user variable "j"
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- arrays ---
[GOOD] (define-fun array_0 () (Array Int Int) ((as const (Array Int Int)) 7))
[GOOD] (declare-fun array_1 () (Array Int Int))
[GOOD] (define-fun array_1_initializer_0 () Bool (= array_1 (store array_0 s3 s15)))
[GOOD] (declare-fun array_2 () (Array Int Int))
[GOOD] (define-fun array_2_initializer_0 () Bool (= array_2 (store array_1 s5 s16)))
[GOOD] (declare-fun array_3 () (Array Int Int))
[GOOD] (define-fun array_3_initializer_0 () Bool (= array_3 (store array_2 s7 s17)))
[GOOD] (declare-fun array_4 () (Array Int Int))
[GOOD] (define-fun array_4_initializer_0 () Bool (= array_4 (store array_3 s9 s16)))
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
Expand All @@ -44,25 +34,14 @@
[GOOD] (define-fun s11 () Bool (or s8 s10))
[GOOD] (define-fun s12 () Bool (or s6 s11))
[GOOD] (define-fun s13 () Bool (or s4 s12))
[GOOD] (define-fun s18 () Int (select array_4 s0))
[GOOD] (define-fun s19 () Int (select array_4 s1))
[GOOD] (define-fun s20 () Bool (= s18 s19))
[GOOD] ; --- arrayDelayeds ---
[GOOD] ; --- arraySetups ---
[GOOD] (define-fun array_0_initializer () Bool true) ; no initialization needed
[GOOD] (define-fun array_1_initializer () Bool array_1_initializer_0)
[GOOD] (assert array_1_initializer)
[GOOD] (define-fun array_2_initializer () Bool array_2_initializer_0)
[GOOD] (assert array_2_initializer)
[GOOD] (define-fun array_3_initializer () Bool array_3_initializer_0)
[GOOD] (assert array_3_initializer)
[GOOD] (define-fun array_4_initializer () Bool array_4_initializer_0)
[GOOD] (assert array_4_initializer)
[GOOD] (define-fun s15 () Int (select s14 s0))
[GOOD] (define-fun s16 () Int (select s14 s1))
[GOOD] (define-fun s17 () Bool (= s15 s16))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert s2)
[GOOD] (assert s13)
[GOOD] (assert s20)
[GOOD] (assert s17)
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
Expand Down
40 changes: 18 additions & 22 deletions SBVTestSuite/GoldFiles/queryArrays1.gold
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,44 +5,40 @@
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-option :pp.max_depth 4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (set-option :model.inline_def true )
[GOOD] (set-logic ALL) ; external query, using all logics.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () (_ BitVec 8)) ; tracks user variable "a1"
[GOOD] (declare-fun s1 () (_ BitVec 8)) ; tracks user variable "a2"
[GOOD] (declare-fun s3 () (_ BitVec 8)) ; tracks user variable "v1"
[GOOD] (declare-fun s0 () (Array (_ BitVec 8) (_ BitVec 8))) ; tracks user variable "a"
[GOOD] (declare-fun s1 () (_ BitVec 8)) ; tracks user variable "a1"
[GOOD] (declare-fun s2 () (_ BitVec 8)) ; tracks user variable "a2"
[GOOD] (declare-fun s4 () (_ BitVec 8)) ; tracks user variable "v1"
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- arrays ---
[GOOD] (declare-fun array_0 () (Array (_ BitVec 8) (_ BitVec 8)))
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s2 () Bool (distinct s0 s1))
[GOOD] ; --- arrayDelayeds ---
[GOOD] ; --- arraySetups ---
[GOOD] (define-fun array_0_initializer () Bool true) ; no initialization needed
[GOOD] (define-fun s3 () Bool (distinct s1 s2))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert s2)
[GOOD] (declare-fun array_1 () (Array (_ BitVec 8) (_ BitVec 8)))
[GOOD] (define-fun s4 () (_ BitVec 8) (select array_1 s0))
[GOOD] (define-fun s5 () Bool (= s3 s4))
[GOOD] (define-fun array_1_initializer_0 () Bool (= array_1 (store array_0 s0 s3)))
[GOOD] (define-fun array_1_initializer () Bool array_1_initializer_0)
[GOOD] (assert array_1_initializer)
[GOOD] (assert s5)
[GOOD] (assert s3)
[GOOD] (define-fun s5 () (Array (_ BitVec 8) (_ BitVec 8)) (store s0 s1 s4))
[GOOD] (define-fun s6 () (_ BitVec 8) (select s5 s1))
[GOOD] (define-fun s7 () Bool (= s4 s6))
[GOOD] (assert s7)
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 #xff))
[SEND] (get-value (s1))
[RECV] ((s1 #x00))
[SEND] (get-value (s3))
[RECV] ((s3 #x00))
[RECV] ((s1 #xff))
[SEND] (get-value (s2))
[RECV] ((s2 #x00))
[SEND] (get-value (s4))
[RECV] ((s4 #x00))
*** Solver : Z3
*** Exit code: ExitSuccess

Expand Down
37 changes: 15 additions & 22 deletions SBVTestSuite/GoldFiles/queryArrays5.gold
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,41 +5,34 @@
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-option :pp.max_depth 4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (set-option :model.inline_def true )
[GOOD] (set-logic ALL) ; external query, using all logics.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () (_ BitVec 8)) ; tracks user variable "a"
[GOOD] (declare-fun s1 () (_ BitVec 8)) ; tracks user variable "v"
[GOOD] (declare-fun s0 () (Array (_ BitVec 8) (_ BitVec 8))) ; tracks user variable "a"
[GOOD] (declare-fun s1 () (_ BitVec 8)) ; tracks user variable "a_0"
[GOOD] (declare-fun s2 () (_ BitVec 8)) ; tracks user variable "v"
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- arrays ---
[GOOD] (declare-fun array_0 () (Array (_ BitVec 8) (_ BitVec 8)))
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] ; --- arrayDelayeds ---
[GOOD] ; --- arraySetups ---
[GOOD] (define-fun array_0_initializer () Bool true) ; no initialization needed
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (define-fun s2 () (_ BitVec 8) #x01)
[GOOD] (define-fun s4 () (_ BitVec 8) #x01)
[GOOD] (declare-fun array_1 () (Array (_ BitVec 8) (_ BitVec 8)))
[GOOD] (declare-fun array_2 () (Array (_ BitVec 8) (_ BitVec 8)))
[GOOD] (define-fun s3 () (_ BitVec 8) (bvadd s1 s2))
[GOOD] (define-fun s5 () (_ BitVec 8) (bvadd s0 s4))
[GOOD] (define-fun s6 () (_ BitVec 8) (select array_2 s5))
[GOOD] (define-fun s7 () Bool (distinct s3 s6))
[GOOD] (define-fun array_1_initializer_0 () Bool (= array_1 (store array_0 s0 s1)))
[GOOD] (define-fun array_2_initializer_0 () Bool (= array_2 (store array_1 s5 s3)))
[GOOD] (define-fun array_1_initializer () Bool array_1_initializer_0)
[GOOD] (assert array_1_initializer)
[GOOD] (define-fun array_2_initializer () Bool array_2_initializer_0)
[GOOD] (assert array_2_initializer)
[GOOD] (assert s7)
[GOOD] (define-fun s3 () (_ BitVec 8) #x01)
[GOOD] (define-fun s6 () (_ BitVec 8) #x01)
[GOOD] (define-fun s4 () (_ BitVec 8) (bvadd s2 s3))
[GOOD] (define-fun s5 () (Array (_ BitVec 8) (_ BitVec 8)) (store s0 s1 s2))
[GOOD] (define-fun s7 () (_ BitVec 8) (bvadd s1 s6))
[GOOD] (define-fun s8 () (Array (_ BitVec 8) (_ BitVec 8)) (store s5 s7 s4))
[GOOD] (define-fun s9 () (_ BitVec 8) (select s8 s7))
[GOOD] (define-fun s10 () Bool (distinct s4 s9))
[GOOD] (assert s10)
[SEND] (check-sat)
[RECV] unsat
*** Solver : Z3
Expand Down
82 changes: 35 additions & 47 deletions SBVTestSuite/GoldFiles/queryArrays6.gold
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,77 +5,65 @@
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-option :pp.max_depth 4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (set-option :model.inline_def true )
[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () (Array Int Int)) ; tracks user variable "a"
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- arrays ---
[GOOD] (declare-fun array_0 () (Array Int Int))
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] ; --- arrayDelayeds ---
[GOOD] ; --- arraySetups ---
[GOOD] (define-fun array_0_initializer () Bool true) ; no initialization needed
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (push 1)
[GOOD] (define-fun s0 () Int 1)
[GOOD] (define-fun s2 () Int 5)
[GOOD] (declare-fun array_1 () (Array Int Int))
[GOOD] (define-fun array_1_initializer_0 () Bool (= array_1 (store array_0 s0 s0)))
[GOOD] (define-fun s1 () Int (select array_1 s0))
[GOOD] (define-fun s3 () Bool (= s1 s2))
[GOOD] (define-fun array_1_initializer () Bool array_1_initializer_0)
[GOOD] (assert array_1_initializer)
[GOOD] (assert s3)
[GOOD] (define-fun s1 () Int 1)
[GOOD] (define-fun s4 () Int 5)
[GOOD] (define-fun s2 () (Array Int Int) (store s0 s1 s1))
[GOOD] (define-fun s3 () Int (select s2 s1))
[GOOD] (define-fun s5 () Bool (= s3 s4))
[GOOD] (assert s5)
[SEND] (check-sat)
[RECV] unsat
[GOOD] (pop 1)
[GOOD] (assert (and array_0_initializer array_1_initializer))
[GOOD] (declare-fun s4 () Int)
[GOOD] (define-fun s6 () Int 3)
[GOOD] (define-fun s5 () Bool (>= s4 s0))
[GOOD] (define-fun s7 () Bool (< s4 s6))
[GOOD] (define-fun s8 () Bool (and s5 s7))
[GOOD] (assert s8)
[GOOD] (declare-fun s6 () Int)
[GOOD] (define-fun s8 () Int 3)
[GOOD] (define-fun s7 () Bool (>= s6 s1))
[GOOD] (define-fun s9 () Bool (< s6 s8))
[GOOD] (define-fun s10 () Bool (and s7 s9))
[GOOD] (assert s10)
[GOOD] (push 1)
[GOOD] (declare-fun array_2 () (Array Int Int))
[GOOD] (define-fun s9 () Int (+ s1 s4))
[GOOD] (define-fun s10 () Int (select array_2 s0))
[GOOD] (define-fun s11 () Bool (= s2 s10))
[GOOD] (define-fun array_2_initializer_0 () Bool (= array_2 (store array_1 s0 s9)))
[GOOD] (define-fun array_2_initializer () Bool array_2_initializer_0)
[GOOD] (assert array_2_initializer)
[GOOD] (assert s11)
[GOOD] (define-fun s11 () Int (+ s3 s6))
[GOOD] (define-fun s12 () (Array Int Int) (store s2 s1 s11))
[GOOD] (define-fun s13 () Int (select s12 s1))
[GOOD] (define-fun s14 () Bool (= s4 s13))
[GOOD] (assert s14)
[SEND] (check-sat)
[RECV] unsat
[GOOD] (pop 1)
[GOOD] (assert (and array_0_initializer array_1_initializer array_2_initializer))
[GOOD] (declare-fun s12 () Int)
[GOOD] (define-fun s13 () Bool (>= s12 s0))
[GOOD] (define-fun s14 () Bool (< s12 s6))
[GOOD] (define-fun s15 () Bool (and s13 s14))
[GOOD] (assert s15)
[GOOD] (push 1)
[GOOD] (declare-fun array_3 () (Array Int Int))
[GOOD] (define-fun s16 () Int (+ s10 s12))
[GOOD] (define-fun s17 () Int (select array_3 s0))
[GOOD] (define-fun s18 () Bool (= s2 s17))
[GOOD] (define-fun array_3_initializer_0 () Bool (= array_3 (store array_2 s0 s16)))
[GOOD] (define-fun array_3_initializer () Bool array_3_initializer_0)
[GOOD] (assert array_3_initializer)
[GOOD] (declare-fun s15 () Int)
[GOOD] (define-fun s16 () Bool (>= s15 s1))
[GOOD] (define-fun s17 () Bool (< s15 s8))
[GOOD] (define-fun s18 () Bool (and s16 s17))
[GOOD] (assert s18)
[GOOD] (push 1)
[GOOD] (define-fun s19 () Int (+ s13 s15))
[GOOD] (define-fun s20 () (Array Int Int) (store s12 s1 s19))
[GOOD] (define-fun s21 () Int (select s20 s1))
[GOOD] (define-fun s22 () Bool (= s4 s21))
[GOOD] (assert s22)
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s4))
[RECV] ((s4 2))
[SEND] (get-value (s12))
[RECV] ((s12 2))
[SEND] (get-value (s6))
[RECV] ((s6 2))
[SEND] (get-value (s15))
[RECV] ((s15 2))
*** Solver : Z3
*** Exit code: ExitSuccess

Expand Down
Loading

0 comments on commit 0d06440

Please sign in to comment.