packages feed

sbv-14.4: SBVTestSuite/GoldFiles/lambda57c.gold

[MEASURE] Verifying termination measures for: f1w @(SBV Word8 -> SBV Word8), f1w @(SBV Word8 -> SBV Word8), f2w @(SBV Word8 -> SBV Word8), f2w @(SBV Word8 -> SBV Word8), f3w @(SBV Word8 -> SBV Word8), f3w @(SBV Word8 -> SBV Word8), f4w @(SBV Word8 -> SBV Word8), f4w @(SBV Word8 -> SBV Word8)
[MEASURE] Checking: f1w @(SBV Word8 -> SBV Word8)
[MEASURE] Checking mutual recursion group: {f1w :: SBV Word8 -> SBV Word8, f2w :: SBV Word8 -> SBV Word8, f3w :: SBV Word8 -> SBV Word8, f4w :: SBV Word8 -> SBV Word8}
[MEASURE] Mutual group: trying user-provided measure for all members
[MEASURE] replayDAG {f1w @(SBV Word8 -> SBV Word8), f2w @(SBV Word8 -> SBV Word8), f3w @(SBV Word8 -> SBV Word8), f4w @(SBV Word8 -> SBV Word8)}: replaying 8 node(s)
** Calling: z3 -nw -in -smt2
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s1 () (_ BitVec 8) #x00)
[GOOD] (define-fun s2 () (_ BitVec 8) #x01)
[GOOD] (define-fun s3 () (_ BitVec 8) #x02)
[GOOD] (define-fun s13 () Int 0)
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () (_ BitVec 8)) ; tracks user variable "arg"
[GOOD] (declare-fun s6 () (_ BitVec 8)) ; tracks user variable "__internal_sbv_s6"
[GOOD] (declare-fun s8 () (_ BitVec 8)) ; tracks user variable "__internal_sbv_s8"
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s4 () Bool (= s0 s1))
[GOOD] (define-fun s5 () (_ BitVec 8) (bvsub s0 s2))
[GOOD] (define-fun s7 () (_ BitVec 8) (bvsub s0 s3))
[GOOD] (define-fun s9 () (_ BitVec 8) (bvadd s6 s8))
[GOOD] (define-fun s10 () (_ BitVec 8) (bvadd s2 s9))
[GOOD] (define-fun s11 () (_ BitVec 8) (ite s4 s1 s10))
[GOOD] (define-fun s12 () Int (ubv_to_int s0))
[GOOD] (define-fun s14 () Bool (>= s12 s13))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert (not s14))
[SEND] (check-sat)
[RECV] unsat
*** Solver   : Z3
*** Exit code: ExitSuccess
[MEASURE] replayDAG {f1w @(SBV Word8 -> SBV Word8), f2w @(SBV Word8 -> SBV Word8), f3w @(SBV Word8 -> SBV Word8), f4w @(SBV Word8 -> SBV Word8)}: replaying 8 node(s)
** Calling: z3 -nw -in -smt2
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s1 () (_ BitVec 8) #x00)
[GOOD] (define-fun s2 () (_ BitVec 8) #x01)
[GOOD] (define-fun s3 () (_ BitVec 8) #x02)
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () (_ BitVec 8)) ; tracks user variable "arg"
[GOOD] (declare-fun s6 () (_ BitVec 8)) ; tracks user variable "__internal_sbv_s6"
[GOOD] (declare-fun s8 () (_ BitVec 8)) ; tracks user variable "__internal_sbv_s8"
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s4 () Bool (= s0 s1))
[GOOD] (define-fun s5 () (_ BitVec 8) (bvsub s0 s2))
[GOOD] (define-fun s7 () (_ BitVec 8) (bvsub s0 s3))
[GOOD] (define-fun s9 () (_ BitVec 8) (bvadd s6 s8))
[GOOD] (define-fun s10 () (_ BitVec 8) (bvadd s2 s9))
[GOOD] (define-fun s11 () (_ BitVec 8) (ite s4 s1 s10))
[GOOD] (define-fun s12 () Int (ubv_to_int s0))
[GOOD] (define-fun s13 () Int (ubv_to_int s5))
[GOOD] (define-fun s14 () Int (ubv_to_int s7))
[GOOD] (define-fun s15 () Bool (not s4))
[GOOD] (define-fun s16 () Bool (> s12 s13))
[GOOD] (define-fun s17 () Bool (=> s15 s16))
[GOOD] (define-fun s18 () Bool (> s12 s14))
[GOOD] (define-fun s19 () Bool (=> s15 s18))
[GOOD] (define-fun s20 () Bool (and s17 s19))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert (not s20))
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s12))
[RECV] ((s12 1))
[SEND] (get-value (s13))
[RECV] ((s13 0))
[SEND] (get-value (s14))
[RECV] ((s14 255))
[SEND] (get-value (s0))
[RECV] ((s0 #x01))
[SEND] (get-value (s6))
[RECV] ((s6 #x00))
[SEND] (get-value (s8))
[RECV] ((s8 #x00))
*** Solver   : Z3
*** Exit code: ExitSuccess
[MEASURE] Mutual group: decrease failed for f1w @(SBV Word8 -> SBV Word8): Falsifiable. Counter-example:
  arg     =   1 :: Word8
  before  =   1 :: Integer
  then[1] =   0 :: Integer
  then[2] = 255 :: Integer
[MEASURE] Mutual group: user-provided measure failed, falling back to auto-guess
[MEASURE] Mutual group: trying measure arg1 for all members
[MEASURE] replayDAG {f1w @(SBV Word8 -> SBV Word8), f2w @(SBV Word8 -> SBV Word8), f3w @(SBV Word8 -> SBV Word8), f4w @(SBV Word8 -> SBV Word8)}: replaying 8 node(s)
** Calling: z3 -nw -in -smt2
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s1 () (_ BitVec 8) #x00)
[GOOD] (define-fun s2 () (_ BitVec 8) #x01)
[GOOD] (define-fun s3 () (_ BitVec 8) #x02)
[GOOD] (define-fun s13 () Int 0)
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () (_ BitVec 8)) ; tracks user variable "arg"
[GOOD] (declare-fun s6 () (_ BitVec 8)) ; tracks user variable "__internal_sbv_s6"
[GOOD] (declare-fun s8 () (_ BitVec 8)) ; tracks user variable "__internal_sbv_s8"
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s4 () Bool (= s0 s1))
[GOOD] (define-fun s5 () (_ BitVec 8) (bvsub s0 s2))
[GOOD] (define-fun s7 () (_ BitVec 8) (bvsub s0 s3))
[GOOD] (define-fun s9 () (_ BitVec 8) (bvadd s6 s8))
[GOOD] (define-fun s10 () (_ BitVec 8) (bvadd s2 s9))
[GOOD] (define-fun s11 () (_ BitVec 8) (ite s4 s1 s10))
[GOOD] (define-fun s12 () Int (ubv_to_int s0))
[GOOD] (define-fun s14 () Bool (>= s12 s13))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert (not s14))
[SEND] (check-sat)
[RECV] unsat
*** Solver   : Z3
*** Exit code: ExitSuccess
[MEASURE] replayDAG {f1w @(SBV Word8 -> SBV Word8), f2w @(SBV Word8 -> SBV Word8), f3w @(SBV Word8 -> SBV Word8), f4w @(SBV Word8 -> SBV Word8)}: replaying 8 node(s)
** Calling: z3 -nw -in -smt2
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s1 () (_ BitVec 8) #x00)
[GOOD] (define-fun s2 () (_ BitVec 8) #x01)
[GOOD] (define-fun s3 () (_ BitVec 8) #x02)
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () (_ BitVec 8)) ; tracks user variable "arg"
[GOOD] (declare-fun s6 () (_ BitVec 8)) ; tracks user variable "__internal_sbv_s6"
[GOOD] (declare-fun s8 () (_ BitVec 8)) ; tracks user variable "__internal_sbv_s8"
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s4 () Bool (= s0 s1))
[GOOD] (define-fun s5 () (_ BitVec 8) (bvsub s0 s2))
[GOOD] (define-fun s7 () (_ BitVec 8) (bvsub s0 s3))
[GOOD] (define-fun s9 () (_ BitVec 8) (bvadd s6 s8))
[GOOD] (define-fun s10 () (_ BitVec 8) (bvadd s2 s9))
[GOOD] (define-fun s11 () (_ BitVec 8) (ite s4 s1 s10))
[GOOD] (define-fun s12 () Int (ubv_to_int s0))
[GOOD] (define-fun s13 () Int (ubv_to_int s5))
[GOOD] (define-fun s14 () Int (ubv_to_int s7))
[GOOD] (define-fun s15 () Bool (not s4))
[GOOD] (define-fun s16 () Bool (> s12 s13))
[GOOD] (define-fun s17 () Bool (=> s15 s16))
[GOOD] (define-fun s18 () Bool (> s12 s14))
[GOOD] (define-fun s19 () Bool (=> s15 s18))
[GOOD] (define-fun s20 () Bool (and s17 s19))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert (not s20))
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s12))
[RECV] ((s12 1))
[SEND] (get-value (s13))
[RECV] ((s13 0))
[SEND] (get-value (s14))
[RECV] ((s14 255))
[SEND] (get-value (s0))
[RECV] ((s0 #x01))
[SEND] (get-value (s6))
[RECV] ((s6 #x00))
[SEND] (get-value (s8))
[RECV] ((s8 #x00))
*** Solver   : Z3
*** Exit code: ExitSuccess
[MEASURE] Mutual group: decrease failed for f1w @(SBV Word8 -> SBV Word8): Falsifiable. Counter-example:
  arg     =   1 :: Word8
  before  =   1 :: Integer
  then[1] =   0 :: Integer
  then[2] = 255 :: Integer
[MEASURE] Mutual group: measure arg1 failed, trying next

EXCEPTION CAUGHT:

*** Data.SBV: Cannot determine a termination measure for mutual recursion group.
***
***     f1w  :: SBV Word8 -> SBV Word8
***     f2w  :: SBV Word8 -> SBV Word8
***     f3w  :: SBV Word8 -> SBV Word8
***     f4w  :: SBV Word8 -> SBV Word8
***
*** The user-provided measure did not work, and auto-guessing also failed.