Skip to content

Instantly share code, notes, and snippets.

@hgvk94

hgvk94/gen32-simple.smt2

Created November 19, 2020 19:55
Show Gist options
  • Save hgvk94/f836e2af2d8c92881dd681697101ac2c to your computer and use it in GitHub Desktop.
Save hgvk94/f836e2af2d8c92881dd681697101ac2c to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gen32-simple.smt2
(set-option :fp.engine spacer)
(set-logic HORN)
(declare-fun Inv (Bool Bool Bool Bool Bool (_ BitVec 512)) Bool)
(declare-fun simple!!query () Bool)
(assert (forall ((i!12 Bool)
(i!11 Bool)
(i!10 Bool)
(i!9 Bool)
(i!8 (_ BitVec 279))
(i!7 Bool)
(i!6 Bool)
(i!5 Bool)
(i!4 (_ BitVec 2))
(i!3 Bool)
(i!2 Bool)
(i!1 Bool)
(i!0 Bool)
(vo!24 (_ BitVec 512))
(vo!22 Bool)
(vo!20 Bool)
(vo!18 Bool)
(vo!16 Bool)
(vo!14 Bool)
(vi!23 (_ BitVec 512))
(vi!21 Bool)
(vi!19 Bool)
(vi!17 Bool)
(vi!15 Bool)
(vi!13 Bool))
(=> (and (not vi!15) (not vi!17) (not vi!19))
(Inv vi!13 vi!15 vi!17 vi!19 vi!21 vi!23))))
(assert (forall ((i!12 Bool)
(i!11 Bool)
(i!10 Bool)
(i!9 Bool)
(i!8 (_ BitVec 279))
(i!7 Bool)
(i!6 Bool)
(i!5 Bool)
(i!4 (_ BitVec 2))
(i!3 Bool)
(i!2 Bool)
(i!1 Bool)
(i!0 Bool)
(vo!24 (_ BitVec 512))
(vo!22 Bool)
(vo!20 Bool)
(vo!18 Bool)
(vo!16 Bool)
(vo!14 Bool)
(vi!23 (_ BitVec 512))
(vi!21 Bool)
(vi!19 Bool)
(vi!17 Bool)
(vi!15 Bool)
(vi!13 Bool))
(let ((a!1 (not (or (= ((_ extract 282 282) vi!23) #b0)
(= ((_ extract 283 283) vi!23) #b0))))
(a!2 (not (or (= ((_ extract 282 282) vi!23) #b0)
(= ((_ extract 284 284) vi!23) #b0))))
(a!3 (not (or (= ((_ extract 283 283) vi!23) #b0)
(= ((_ extract 284 284) vi!23) #b0))))
(a!8 (and i!7 (not (and (not i!10) (not i!11))) (not i!5)))
(a!13 (not (or (and i!2 (not i!3)) (not i!3) i!0)))
(a!16 (bvor (bvnot ((_ extract 278 271) i!8))
(concat (bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1)))))
(a!17 (bvor (bvnot ((_ extract 270 265) i!8))
(concat (bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1)))))
(a!18 (bvor (bvnot ((_ extract 264 0) i!8))
(concat (bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))
(bvnot (ite i!9 #b0 #b1))))))
(let ((a!4 (and (not i!2) (not i!5) (not (or a!1 a!2 a!3))))
(a!6 (ite (= i!4 #b01)
(and (not i!2) (not i!5))
(and (not i!2) (not i!5) (or a!1 a!2 a!3 (and i!6 vi!21)))))
(a!19 (concat #x00000000000000000000000000000000000000000000000000000000
(ite i!3
#x000000000000000000000000000000000000000000000000000000000000000000000000
(concat (bvnot a!16)
#b00
(bvnot a!17)
#b0000000
(bvnot a!18))))))
(let ((a!5 (ite (= i!4 #b11)
(and (not i!7) (not i!2) (not i!5) (not (or a!1 a!2 a!3)))
a!4))
(a!9 (and (or (= i!4 #b10) (= i!4 #b11))
(ite (= i!4 #b11) a!8 (and (not a!4) (not i!5) i!6 i!10)))))
(let ((a!7 (ite (or (= i!4 #b10) (= i!4 #b11)) a!5 a!6)))
(let ((a!10 (ite i!1 (and (not i!0) (ite (or a!7 a!9) vi!21 vi!13)) vi!13))
(a!11 (ite i!1 (ite (or i!0 a!7 a!9) (and (not i!0) vi!17) vi!15) vi!15))
(a!12 (ite i!1 (ite (or i!0 a!7 a!9) (and (not i!0) vi!19) vi!17) vi!17))
(a!14 (ite (or i!0 (and i!2 (not i!3)) a!7) a!13 vi!19))
(a!15 (ite i!1
(and (not i!0) (ite (or a!7 a!9) (or a!1 a!2 a!3) vi!21))
vi!21))
(a!20 (ite i!0
#x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
(ite (and i!2 (not i!3))
(concat #x00000000000000000000000000000000000000000000000000000000
(bvnot a!16)
#b00
(bvnot a!17)
#b0000000
(bvnot a!18))
(ite a!7 a!19 vi!23)))))
(=> (and (Inv vi!13 vi!15 vi!17 vi!19 vi!21 vi!23)
(= vo!14 a!10)
(= vo!16 a!11)
(= vo!18 a!12)
(= vo!20 (ite i!1 a!14 vi!19))
(= vo!22 a!15)
(= vo!24 (ite i!1 a!20 vi!23)))
(Inv vo!14 vo!16 vo!18 vo!20 vo!22 vo!24)))))))))
(assert (forall ((vi!13 Bool)
(vi!15 Bool)
(vi!17 Bool)
(vi!19 Bool)
(vi!21 Bool)
(vi!23 (_ BitVec 512))
(vo!14 Bool)
(vo!16 Bool)
(vo!18 Bool)
(vo!20 Bool)
(vo!22 Bool)
(vo!24 (_ BitVec 512))
(i!0 Bool)
(i!1 Bool)
(i!2 Bool)
(i!3 Bool)
(i!4 (_ BitVec 2))
(i!5 Bool)
(i!6 Bool)
(i!7 Bool)
(i!8 (_ BitVec 279))
(i!9 Bool)
(i!10 Bool)
(i!11 Bool)
(i!12 Bool))
(=> (and (Inv vi!13 vi!15 vi!17 vi!19 vi!21 vi!23) vi!15 vi!13) simple!!query)))
(assert (=> simple!!query false))
(check-sat)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment