Skip to content

Instantly share code, notes, and snippets.

/encodingA.smt2

Created June 11, 2012 08:11
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save anonymous/2909024 to your computer and use it in GitHub Desktop.
Save anonymous/2909024 to your computer and use it in GitHub Desktop.
Download ZIP
Follow-up to gist 2895551
Raw
encodingA.smt2
(assert (not (or (= 1.0 0.74) (< 0.74 1.0))))
(assert (not (or (= 0.01 0.0) (< 0.0 0.01))))
(assert (not (or (= 1.0 0.02) (< 0.02 1.0))))
(assert (< $FAppRd@67 0.01))
(assert (not (or (= 1.0 (+ 0.01 (* 0.01 $FAppRd@67))) (< (+ 0.01 (* 0.01 $FAppRd@67)) 1.0))))
(assert (< $FAppRd@76 (* 0.01 $FAppRd@67)))
(assert (< $FAppRd@87 0.01))
(assert (not (or (= 1.0 (+ 0.01 (* 0.01 $FAppRd@87))) (< (+ 0.01 (* 0.01 $FAppRd@87)) 1.0))))
(assert (< $FAppRd@96 (* 0.01 $FAppRd@87)))
(assert (< $FAppRd@107 0.01))
(assert (not (or (= 1.0 (+ 0.01 (* 0.01 $FAppRd@107))) (< (+ 0.01 (* 0.01 $FAppRd@107)) 1.0))))
(assert (< $FAppRd@116 (* 0.01 $FAppRd@107)))
(assert (< $FAppRd@127 0.01))
(assert (not (or (= 1.0 (+ 0.01 (* 0.01 $FAppRd@127))) (< (+ 0.01 (* 0.01 $FAppRd@127)) 1.0))))
(assert (< $FAppRd@136 (* 0.01 $FAppRd@127)))
(assert (< $FAppRd@147 0.01))
(assert (not (or (= 1.0 (+ 0.01 (* 0.01 $FAppRd@147))) (< (+ 0.01 (* 0.01 $FAppRd@147)) 1.0))))
(assert (< $FAppRd@156 (* 0.01 $FAppRd@147)))
(assert (< $FAppRd@167 0.01))
(assert (not (or (= 1.0 (+ 0.01 (* 0.01 $FAppRd@167))) (< (+ 0.01 (* 0.01 $FAppRd@167)) 1.0))))
(assert (< $FAppRd@176 (* 0.01 $FAppRd@167)))
(assert (< $FAppRd@187 0.01))
(assert (not (or (= 1.0 (+ 0.01 (* 0.01 $FAppRd@187))) (< (+ 0.01 (* 0.01 $FAppRd@187)) 1.0))))
(assert (< $FAppRd@196 (* 0.01 $FAppRd@187)))
(assert (not (or (= 1.0 (+ (* 0.01 $MethRd@200) $MethRd@200)) (< (+ (* 0.01 $MethRd@200) $MethRd@200) 1.0))))
(assert (< $FAppRd@217 (* 0.01 $MethRd@200)))
(assert (not (or (= 1.0 (+ (* 0.01 $FAppRd@217) (* 0.01 $MethRd@200))) (< (+ (* 0.01 $FAppRd@217) (* 0.01 $MethRd@200)) 1.0))))
(assert (not (or (= 1.0 (+ (* 0.01 $FAppRd@217) $MethRd@200)) (< (+ (* 0.01 $FAppRd@217) $MethRd@200) 1.0))))
(assert (< $FAppRd@226 (* 0.01 $FAppRd@217)))
(assert (not (or (= 1.0 (+ $MethRd@200 (* 0.01 $FAppRd@217))) (< (+ $MethRd@200 (* 0.01 $FAppRd@217)) 1.0))))
(assert (not (or (= 1.0 (+ $MethRd@200 (* 0.01 $MethRd@200))) (< (+ $MethRd@200 (* 0.01 $MethRd@200)) 1.0))))
(assert (not (or (= 1.0 (+ (* 0.01 $MethRd@200) (* 0.01 $FAppRd@217))) (< (+ (* 0.01 $MethRd@200) (* 0.01 $FAppRd@217)) 1.0))))
Raw
encodingB.smt2
(assert (not (or (= 1.0 (+ 0.75 (- 0.0 $Perms.pRd))) (< (+ 0.75 (- 0.0 $Perms.pRd)) 1.0))))
(assert (not (or (= 1.0 (+ $Perms.pRd $Perms.pRd)) (< (+ $Perms.pRd $Perms.pRd) 1.0))))
(assert (< $FAppRd@67 $Perms.pRd))
(assert (not (or (= 1.0 (+ (* $Perms.pRd $FAppRd@67) $Perms.pRd)) (< (+ (* $Perms.pRd $FAppRd@67) $Perms.pRd) 1.0))))
(assert (< $FAppRd@76 (* $Perms.pRd $FAppRd@67)))
(assert (not (or (= 1.0 (+ $Perms.pRd (* $Perms.pRd $FAppRd@67))) (< (+ $Perms.pRd (* $Perms.pRd $FAppRd@67)) 1.0))))
(assert (< $FAppRd@87 $Perms.pRd))
(assert (not (or (= 1.0 (+ (* $Perms.pRd $FAppRd@87) $Perms.pRd)) (< (+ (* $Perms.pRd $FAppRd@87) $Perms.pRd) 1.0))))
(assert (< $FAppRd@96 (* $Perms.pRd $FAppRd@87)))
(assert (not (or (= 1.0 (+ $Perms.pRd (* $Perms.pRd $FAppRd@87))) (< (+ $Perms.pRd (* $Perms.pRd $FAppRd@87)) 1.0))))
(assert (< $FAppRd@107 $Perms.pRd))
(assert (not (or (= 1.0 (+ (* $Perms.pRd $FAppRd@107) $Perms.pRd)) (< (+ (* $Perms.pRd $FAppRd@107) $Perms.pRd) 1.0))))
(assert (< $FAppRd@116 (* $Perms.pRd $FAppRd@107)))
(assert (not (or (= 1.0 (+ $Perms.pRd (* $Perms.pRd $FAppRd@107))) (< (+ $Perms.pRd (* $Perms.pRd $FAppRd@107)) 1.0))))
(assert (< $FAppRd@127 $Perms.pRd))
(assert (not (or (= 1.0 (+ (* $Perms.pRd $FAppRd@127) $Perms.pRd)) (< (+ (* $Perms.pRd $FAppRd@127) $Perms.pRd) 1.0))))
(assert (< $FAppRd@136 (* $Perms.pRd $FAppRd@127)))
(assert (not (or (= 1.0 (+ $Perms.pRd (* $Perms.pRd $FAppRd@127))) (< (+ $Perms.pRd (* $Perms.pRd $FAppRd@127)) 1.0))))
(assert (< $FAppRd@147 $Perms.pRd))
(assert (not (or (= 1.0 (+ (* $Perms.pRd $FAppRd@147) $Perms.pRd)) (< (+ (* $Perms.pRd $FAppRd@147) $Perms.pRd) 1.0))))
(assert (< $FAppRd@156 (* $Perms.pRd $FAppRd@147)))
(assert (not (or (= 1.0 (+ $Perms.pRd (* $Perms.pRd $FAppRd@147))) (< (+ $Perms.pRd (* $Perms.pRd $FAppRd@147)) 1.0))))
(assert (< $FAppRd@167 $Perms.pRd))
(assert (not (or (= 1.0 (+ (* $Perms.pRd $FAppRd@167) $Perms.pRd)) (< (+ (* $Perms.pRd $FAppRd@167) $Perms.pRd) 1.0))))
(assert (< $FAppRd@176 (* $Perms.pRd $FAppRd@167)))
(assert (not (or (= 1.0 (+ $Perms.pRd (* $Perms.pRd $FAppRd@167))) (< (+ $Perms.pRd (* $Perms.pRd $FAppRd@167)) 1.0))))
(assert (< $FAppRd@187 $Perms.pRd))
(assert (not (or (= 1.0 (+ (* $Perms.pRd $FAppRd@187) $Perms.pRd)) (< (+ (* $Perms.pRd $FAppRd@187) $Perms.pRd) 1.0))))
(assert (< $FAppRd@196 (* $Perms.pRd $FAppRd@187)))
(assert (not (or (= 1.0 (+ $Perms.pRd (* $Perms.pRd $FAppRd@187))) (< (+ $Perms.pRd (* $Perms.pRd $FAppRd@187)) 1.0))))
(assert (not (or (= 1.0 (+ (* $Perms.pRd $MethRd@200) $MethRd@200)) (< (+ (* $Perms.pRd $MethRd@200) $MethRd@200) 1.0))))
(assert (< $FAppRd@217 (* $Perms.pRd $MethRd@200)))
(assert (not (or (= 1.0 (+ (* $Perms.pRd $FAppRd@217) (* $Perms.pRd $MethRd@200))) (< (+ (* $Perms.pRd $FAppRd@217) (* $Perms.pRd $MethRd@200)) 1.0))))
(assert (not (or (= 1.0 (+ (* $Perms.pRd $FAppRd@217) $MethRd@200)) (< (+ (* $Perms.pRd $FAppRd@217) $MethRd@200) 1.0))))
(assert (< $FAppRd@226 (* $Perms.pRd $FAppRd@217)))
(assert (not (or (= 1.0 (+ (* $Perms.pRd $MethRd@200) (* $Perms.pRd $FAppRd@217))) (< (+ (* $Perms.pRd $MethRd@200) (* $Perms.pRd $FAppRd@217)) 1.0))))
(assert (not (or (= 1.0 (+ $MethRd@200 (* $Perms.pRd $MethRd@200))) (< (+ $MethRd@200 (* $Perms.pRd $MethRd@200)) 1.0))))
(assert (not (or (= 1.0 (+ $MethRd@200 (* $Perms.pRd $FAppRd@217))) (< (+ $MethRd@200 (* $Perms.pRd $FAppRd@217)) 1.0))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment