Skip to content
GitLab
Commit 89315f6b authored by Mathias Preiner's avatar Mathias Preiner
Browse files

Squashed commit of the following: 

commit 83988b56
Author: Mathias Preiner <mathias.preiner@gmail.com>
Date:   Thu May 2 16:53:38 2019 -0700

    Update README.md.

commit f0c2d57e
Author: Mathias Preiner <mathias.preiner@gmail.com>
Date:   Tue Apr 30 15:18:06 2019 -0700

    Update status.

commit 1c79069d
Author: Mathias Preiner <mathias.preiner@gmail.com>
Date:   Tue Apr 23 14:24:51 2019 -0700

    Update status.
parent 4a9314f6
Expand all Hide whitespace changes
Inline Side-by-side
20170501-Heizmann-UltimateAutomizer/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c.smt2
View file @ 89315f6b
......@@ -20750,24 +20750,24 @@ Checking for People Who Love Automata. CAV 2013:36-52
(pop 1)
(push 1)
(assert (forall ((ssl3_connect_~ag_Y~3 (_ BitVec 32))) (not (= (bvadd (bvadd (bvmul c_ssl3_connect_~ag_X~3 ssl3_connect_~ag_Y~3) c_ssl3_connect_~ag_Z~3) (_ bv4294962863 32)) (_ bv0 32)))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (not (forall ((ssl3_connect_~ag_Y~3 (_ BitVec 32))) (not (= (bvadd (bvadd (bvmul c_ssl3_connect_~ag_X~3 ssl3_connect_~ag_Y~3) c_ssl3_connect_~ag_Z~3) (_ bv4294962863 32)) (_ bv0 32))))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (forall ((ssl3_connect_~ag_Y~3 (_ BitVec 32))) (not (= (bvadd (bvadd (bvmul c_ssl3_connect_~ag_X~3 ssl3_connect_~ag_Y~3) c_ssl3_connect_~ag_Z~3) (_ bv4294962863 32)) (_ bv0 32)))))
(assert (= (bvadd c_ssl3_connect_~s__state~3 (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (distinct (bvadd c_ssl3_connect_~s__state~3 (_ bv4294962863 32)) (_ bv0 32)))
(assert (not (forall ((ssl3_connect_~ag_Y~3 (_ BitVec 32))) (not (= (bvadd (bvadd (bvmul c_ssl3_connect_~ag_X~3 ssl3_connect_~ag_Y~3) c_ssl3_connect_~ag_Z~3) (_ bv4294962863 32)) (_ bv0 32))))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
......@@ -20775,12 +20775,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_X~3_const_1938140606 () (_ BitVec 32))
(push 1)
(assert (not (forall ((ssl3_connect_~ag_Y~3 (_ BitVec 32))) (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (forall ((ssl3_connect_~ag_Y~3 (_ BitVec 32))) (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -20790,12 +20790,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -20805,12 +20805,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -20820,12 +20820,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -20835,12 +20835,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -20850,12 +20850,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -20865,12 +20865,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -20880,12 +20880,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -20895,12 +20895,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -20910,12 +20910,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -20925,12 +20925,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -20940,12 +20940,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -20955,12 +20955,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -20970,12 +20970,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -20985,12 +20985,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -21000,12 +21000,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -21015,12 +21015,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -21030,12 +21030,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -21045,12 +21045,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -21060,12 +21060,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -21075,12 +21075,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -21090,12 +21090,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -21105,12 +21105,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -21120,12 +21120,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -21135,12 +21135,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Z~3_const_1938183228 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul ssl3_connect_~ag_X~3_const_1938140606 ssl3_connect_~ag_Y~3_const_1938182653) ssl3_connect_~ag_Z~3_const_1938183228) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......@@ -21150,12 +21150,12 @@ Checking for People Who Love Automata. CAV 2013:36-52
(declare-fun ssl3_connect_~ag_Y~3_const_1938182653 () (_ BitVec 32))
(push 1)
(assert (not (= (bvadd (bvadd (bvmul (_ bv44 32) ssl3_connect_~ag_Y~3_const_1938182653) (bvshl ssl3_connect_~ag_V~3_const_1938138424 ssl3_connect_~ag_W~3_const_1938139519)) (_ bv4294962863 32)) (_ bv0 32))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (= (bvadd (bvadd (bvmul (_ bv44 32) ssl3_connect_~ag_Y~3_const_1938182653) (bvshl ssl3_connect_~ag_V~3_const_1938138424 ssl3_connect_~ag_W~3_const_1938139519)) (_ bv4294962863 32)) (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
......
20170501-Heizmann-UltimateAutomizer/sum02_true-unreach-call_true-no-overflow.i.smt2
View file @ 89315f6b
......@@ -1582,48 +1582,48 @@ Checking for People Who Love Automata. CAV 2013:36-52
(pop 1)
(push 1)
(assert (or (forall ((main_~n~6 (_ BitVec 32))) (or (not (bvule c_main_~i~6 main_~n~6)) (= (bvudiv (bvmul ((_ zero_extend 32) main_~n~6) (bvadd ((_ zero_extend 32) main_~n~6) (_ bv1 64))) (_ bv2 64)) (bvadd c_main_~sn~6 ((_ zero_extend 32) c_main_~i~6))) (bvule (bvadd c_main_~i~6 (_ bv1 32)) main_~n~6))) (= (bvadd c_main_~sn~6 ((_ zero_extend 32) c_main_~i~6)) ((_ sign_extend 32) (_ bv0 32)))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (not (or (forall ((main_~n~6 (_ BitVec 32))) (or (not (bvule c_main_~i~6 main_~n~6)) (= (bvudiv (bvmul ((_ zero_extend 32) main_~n~6) (bvadd ((_ zero_extend 32) main_~n~6) (_ bv1 64))) (_ bv2 64)) (bvadd c_main_~sn~6 ((_ zero_extend 32) c_main_~i~6))) (bvule (bvadd c_main_~i~6 (_ bv1 32)) main_~n~6))) (= (bvadd c_main_~sn~6 ((_ zero_extend 32) c_main_~i~6)) ((_ sign_extend 32) (_ bv0 32))))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (or (forall ((main_~n~6 (_ BitVec 32))) (or (not (bvule c_main_~i~6 main_~n~6)) (= (bvudiv (bvmul ((_ zero_extend 32) main_~n~6) (bvadd ((_ zero_extend 32) main_~n~6) (_ bv1 64))) (_ bv2 64)) (bvadd c_main_~sn~6 ((_ zero_extend 32) c_main_~i~6))) (bvule (bvadd c_main_~i~6 (_ bv1 32)) main_~n~6))) (= (bvadd c_main_~sn~6 ((_ zero_extend 32) c_main_~i~6)) ((_ sign_extend 32) (_ bv0 32)))))
(assert (= c___VERIFIER_assert_~cond (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (distinct c___VERIFIER_assert_~cond (_ bv0 32)))
(assert (not (or (forall ((main_~n~6 (_ BitVec 32))) (or (not (bvule c_main_~i~6 main_~n~6)) (= (bvudiv (bvmul ((_ zero_extend 32) main_~n~6) (bvadd ((_ zero_extend 32) main_~n~6) (_ bv1 64))) (_ bv2 64)) (bvadd c_main_~sn~6 ((_ zero_extend 32) c_main_~i~6))) (bvule (bvadd c_main_~i~6 (_ bv1 32)) main_~n~6))) (= (bvadd c_main_~sn~6 ((_ zero_extend 32) c_main_~i~6)) ((_ sign_extend 32) (_ bv0 32))))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (or (forall ((main_~n~6 (_ BitVec 32))) (or (not (bvule c_main_~i~6 main_~n~6)) (= (bvudiv (bvmul ((_ zero_extend 32) main_~n~6) (bvadd ((_ zero_extend 32) main_~n~6) (_ bv1 64))) (_ bv2 64)) (bvadd c_main_~sn~6 ((_ zero_extend 32) c_main_~i~6))) (bvule (bvadd c_main_~i~6 (_ bv1 32)) main_~n~6))) (= (bvadd c_main_~sn~6 ((_ zero_extend 32) c_main_~i~6)) ((_ sign_extend 32) (_ bv0 32)))))
(assert (= |c___VERIFIER_assert_#in~cond| (_ bv0 32)))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (distinct |c___VERIFIER_assert_#in~cond| (_ bv0 32)))
(assert (not (or (forall ((main_~n~6 (_ BitVec 32))) (or (not (bvule c_main_~i~6 main_~n~6)) (= (bvudiv (bvmul ((_ zero_extend 32) main_~n~6) (bvadd ((_ zero_extend 32) main_~n~6) (_ bv1 64))) (_ bv2 64)) (bvadd c_main_~sn~6 ((_ zero_extend 32) c_main_~i~6))) (bvule (bvadd c_main_~i~6 (_ bv1 32)) main_~n~6))) (= (bvadd c_main_~sn~6 ((_ zero_extend 32) c_main_~i~6)) ((_ sign_extend 32) (_ bv0 32))))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (or (forall ((main_~n~6 (_ BitVec 32))) (or (not (bvule c_main_~i~6 main_~n~6)) (= (bvudiv (bvmul ((_ zero_extend 32) main_~n~6) (bvadd ((_ zero_extend 32) main_~n~6) (_ bv1 64))) (_ bv2 64)) (bvadd c_main_~sn~6 ((_ zero_extend 32) c_main_~i~6))) (bvule (bvadd c_main_~i~6 (_ bv1 32)) main_~n~6))) (= (bvadd c_main_~sn~6 ((_ zero_extend 32) c_main_~i~6)) ((_ sign_extend 32) (_ bv0 32)))))
(assert (not (or (= ((_ sign_extend 32) (_ bv0 32)) c_main_~sn~6) (= c_main_~sn~6 c_main_~gauss~6))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert (or (= ((_ sign_extend 32) (_ bv0 32)) c_main_~sn~6) (= c_main_~sn~6 c_main_~gauss~6)))
(assert (not (or (forall ((main_~n~6 (_ BitVec 32))) (or (not (bvule c_main_~i~6 main_~n~6)) (= (bvudiv (bvmul ((_ zero_extend 32) main_~n~6) (bvadd ((_ zero_extend 32) main_~n~6) (_ bv1 64))) (_ bv2 64)) (bvadd c_main_~sn~6 ((_ zero_extend 32) c_main_~i~6))) (bvule (bvadd c_main_~i~6 (_ bv1 32)) main_~n~6))) (= (bvadd c_main_~sn~6 ((_ zero_extend 32) c_main_~i~6)) ((_ sign_extend 32) (_ bv0 32))))))
(set-info :status unknown)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
......
README.md
View file @ 89315f6b
PLEASE do not use the download button on the top right; use this link instead: http://smt-lib.loria.fr/zip/BV-inc.zip
**Please** **do** **not** use the download button on the top right; use this link
instead:
[http://smt-lib.loria.fr/zip/BV-inc.zip](http://smt-lib.loria.fr/zip/BV-inc.zip)
This is a repository of SMT-LIB benchmarks. See http://smtlib.org/ for more information about the SMT-LIB initiative.
This is a repository of SMT-LIB benchmarks.
See [http://smtlib.org](http://smtlib.org) for more information about the
SMT-LIB initiative.
This repository contains the incremental benchmarks in BV logic. See http://smtlib.org/logics.shtml for a description of the SMT-LIB logics.
This repository contains the incremental benchmarks in BV logic.
See http://smtlib.org/logics.shtml for a description of the SMT-LIB logics.
The benchmarks in this repository are distributed under the [Creative Commons Attribution 4.0 International License](https://creativecommons.org/licenses/by/4.0/
), unless otherwise specified in the benchmark itself (see :license info attribute in the file). If your benchmarks are included in this repository and you do not agree with this licence, please contact [the SMT-LIB co-ordinators] (http://smtlib.org/contact.shtml ).
## Cloning the repository
To clone this repository on your computer, use the git command:
```
git clone https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks-inc/BV.git
```
**Note**: Benchmarks with a size of 10MB+ are stored via
[Git LFS](https://git-lfs.github.com/).
Make sure to install and setup Git LFS before cloning the repository.
## License
The benchmarks in this repository are distributed under the
[Creative Commons Attribution 4.0 International License](https://creativecommons.org/licenses/by/4.0/),
unless otherwise specified in the benchmark itself
(see `:license` info attribute in the file).
If your benchmarks are included in this repository and you do not agree with
this licence, please contact the
[SMT-LIB co-ordinators](http://smtlib.org/contact.shtml).
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment