From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 1 Dec 2009 18:43:20 +0000 (+0000)
Subject: added crypto tests
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=27211b7d79376f9f12023a38192eaa3991caad01;p=francis%2Fstp.git

added crypto tests

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@434 e59a4935-1847-0410-ae03-e826735625c1
---

diff --git a/tests/crypto-tests/t3.stp b/tests/crypto-tests/t3.stp
new file mode 100644
index 0000000..24c2753
--- /dev/null
+++ b/tests/crypto-tests/t3.stp
@@ -0,0 +1,30 @@
+
+a,b,c,x,y : BITVECTOR(48);
+
+ASSERT(y=BVDIV(48,c,a));
+
+
+ASSERT(a[0:0] = 0bin1);
+ASSERT(b[0:0] = 0bin1);
+ASSERT(c=0hex0056E35E38CD);
+
+
+QUERY(
+   NOT (
+     c=BVMULT(48,a,b) AND NOT
+     a=0hex000000000001
+     AND 
+     NOT
+     b=0hex000000000001
+     AND NOT
+     a=c
+     AND NOT
+     b=c
+     AND NOT
+     BVGT(b,y)
+     
+   )
+);
+
+COUNTEREXAMPLE;
+
diff --git a/tests/crypto-tests/t4_nadia.stp b/tests/crypto-tests/t4_nadia.stp
new file mode 100644
index 0000000..4fcca23
--- /dev/null
+++ b/tests/crypto-tests/t4_nadia.stp
@@ -0,0 +1,253 @@
+
+a,b,c,x,y : BITVECTOR(432);
+
+%ASSERT(y=BVDIV(216,c,a));
+
+
+ASSERT(a[0:0] = 0bin1);
+ASSERT(a[1:1] = 0bin1);
+ASSERT(a[2:2] = 0bin1);
+% ASSERT(a[3:3] = 0bin0);
+% ASSERT(a[4:4] = 0bin0);
+ASSERT(a[5:5] = 0bin1);
+% ASSERT(a[6:6] = 0bin0);
+% ASSERT(a[7:7] = 0bin0);
+% ASSERT(a[8:8] = 0bin0);
+% ASSERT(a[9:9] = 0bin0);
+ASSERT(a[10:10] = 0bin1);
+ASSERT(a[11:11] = 0bin1);
+% ASSERT(a[12:12] = 0bin0);
+% ASSERT(a[13:13] = 0bin0);
+% ASSERT(a[14:14] = 0bin0);
+ASSERT(a[15:15] = 0bin1);
+% ASSERT(a[16:16] = 0bin0);
+% ASSERT(a[17:17] = 0bin0);
+% ASSERT(a[18:18] = 0bin0);
+% ASSERT(a[19:19] = 0bin0);
+% ASSERT(a[20:20] = 0bin0);
+% ASSERT(a[21:21] = 0bin0);
+% ASSERT(a[22:22] = 0bin0);
+% ASSERT(a[23:23] = 0bin0);
+% ASSERT(a[24:24] = 0bin0);
+% ASSERT(a[25:25] = 0bin0);
+ASSERT(a[26:26] = 0bin1);
+% ASSERT(a[27:27] = 0bin0);
+ASSERT(a[28:28] = 0bin1);
+% ASSERT(a[29:29] = 0bin0);
+% ASSERT(a[30:30] = 0bin0);
+ASSERT(a[31:31] = 0bin1);
+ASSERT(a[32:32] = 0bin1);
+ASSERT(a[33:33] = 0bin1);
+% ASSERT(a[34:34] = 0bin0);
+ASSERT(a[35:35] = 0bin1);
+% ASSERT(a[36:36] = 0bin0);
+% ASSERT(a[37:37] = 0bin0);
+ASSERT(a[38:38] = 0bin1);
+% ASSERT(a[39:39] = 0bin0);
+% ASSERT(a[40:40] = 0bin0);
+ASSERT(a[41:41] = 0bin1);
+ASSERT(a[42:42] = 0bin1);
+ASSERT(a[43:43] = 0bin1);
+% ASSERT(a[44:44] = 0bin0);
+ASSERT(a[45:45] = 0bin1);
+% ASSERT(a[46:46] = 0bin0);
+% ASSERT(a[47:47] = 0bin0);
+% ASSERT(a[48:48] = 0bin0);
+% ASSERT(a[49:49] = 0bin0);
+% ASSERT(a[50:50] = 0bin0);
+ASSERT(a[51:51] = 0bin1);
+ASSERT(a[52:52] = 0bin1);
+ASSERT(a[53:53] = 0bin1);
+% ASSERT(a[54:54] = 0bin0);
+ASSERT(a[55:55] = 0bin1);
+% ASSERT(a[56:56] = 0bin0);
+% ASSERT(a[57:57] = 0bin0);
+ASSERT(a[58:58] = 0bin1);
+ASSERT(a[59:59] = 0bin1);
+ASSERT(a[60:60] = 0bin1);
+% ASSERT(a[61:61] = 0bin0);
+% ASSERT(a[62:62] = 0bin0);
+% ASSERT(a[63:63] = 0bin0);
+% ASSERT(a[64:64] = 0bin0);
+% ASSERT(a[65:65] = 0bin0);
+ASSERT(a[66:66] = 0bin1);
+% ASSERT(a[67:67] = 0bin0);
+% ASSERT(a[68:68] = 0bin0);
+% ASSERT(a[69:69] = 0bin0);
+% ASSERT(a[70:70] = 0bin0);
+% ASSERT(a[71:71] = 0bin0);
+% ASSERT(a[72:72] = 0bin0);
+% ASSERT(a[73:73] = 0bin0);
+% ASSERT(a[74:74] = 0bin0);
+ASSERT(a[75:75] = 0bin1);
+ASSERT(a[76:76] = 0bin1);
+% ASSERT(a[77:77] = 0bin0);
+ASSERT(a[78:78] = 0bin1);
+% ASSERT(a[79:79] = 0bin0);
+% ASSERT(a[80:80] = 0bin0);
+% ASSERT(a[81:81] = 0bin0);
+ASSERT(a[82:82] = 0bin1);
+ASSERT(a[83:83] = 0bin1);
+ASSERT(a[84:84] = 0bin1);
+% ASSERT(a[85:85] = 0bin0);
+ASSERT(a[86:86] = 0bin1);
+ASSERT(a[87:87] = 0bin1);
+% ASSERT(a[88:88] = 0bin0);
+% ASSERT(a[89:89] = 0bin0);
+% ASSERT(a[90:90] = 0bin0);
+ASSERT(a[91:91] = 0bin1);
+% ASSERT(a[92:92] = 0bin0);
+ASSERT(a[93:93] = 0bin1);
+ASSERT(a[94:94] = 0bin1);
+% ASSERT(a[95:95] = 0bin0);
+ASSERT(a[96:96] = 0bin1);
+ASSERT(a[97:97] = 0bin1);
+% ASSERT(a[98:98] = 0bin0);
+% ASSERT(a[99:99] = 0bin0);
+% ASSERT(a[100:100] = 0bin0);
+
+
+ASSERT(b[0:0] = 0bin1);
+ASSERT(b[1:1] = 0bin1);
+% ASSERT(b[2:2] = 0bin0);
+% ASSERT(b[3:3] = 0bin0);
+ASSERT(b[4:4] = 0bin1);
+ASSERT(b[5:5] = 0bin1);
+ASSERT(b[6:6] = 0bin1);
+% ASSERT(b[7:7] = 0bin0);
+ASSERT(b[8:8] = 0bin1);
+ASSERT(b[9:9] = 0bin1);
+% ASSERT(b[10:10] = 0bin0);
+ASSERT(b[11:11] = 0bin1);
+% ASSERT(b[12:12] = 0bin0);
+% ASSERT(b[13:13] = 0bin0);
+% ASSERT(b[14:14] = 0bin0);
+ASSERT(b[15:15] = 0bin1);
+% ASSERT(b[16:16] = 0bin0);
+% ASSERT(b[17:17] = 0bin0);
+% ASSERT(b[18:18] = 0bin0);
+% ASSERT(b[19:19] = 0bin0);
+% ASSERT(b[20:20] = 0bin0);
+% ASSERT(b[21:21] = 0bin0);
+% ASSERT(b[22:22] = 0bin0);
+% ASSERT(b[23:23] = 0bin0);
+% ASSERT(b[24:24] = 0bin0);
+% ASSERT(b[25:25] = 0bin0);
+ASSERT(b[26:26] = 0bin1);
+% ASSERT(b[27:27] = 0bin0);
+ASSERT(b[28:28] = 0bin1);
+% ASSERT(b[29:29] = 0bin0);
+% ASSERT(b[30:30] = 0bin0);
+% ASSERT(b[31:31] = 0bin0);
+% ASSERT(b[32:32] = 0bin0);
+% ASSERT(b[33:33] = 0bin0);
+% ASSERT(b[34:34] = 0bin0);
+% ASSERT(b[35:35] = 0bin0);
+% ASSERT(b[36:36] = 0bin0);
+ASSERT(b[37:37] = 0bin1);
+ASSERT(b[38:38] = 0bin1);
+% ASSERT(b[39:39] = 0bin0);
+ASSERT(b[40:40] = 0bin1);
+ASSERT(b[41:41] = 0bin1);
+ASSERT(b[42:42] = 0bin1);
+ASSERT(b[43:43] = 0bin1);
+% ASSERT(b[44:44] = 0bin0);
+ASSERT(b[45:45] = 0bin1);
+ASSERT(b[46:46] = 0bin1);
+ASSERT(b[47:47] = 0bin1);
+% ASSERT(b[48:48] = 0bin0);
+ASSERT(b[49:49] = 0bin1);
+ASSERT(b[50:50] = 0bin1);
+% ASSERT(b[51:51] = 0bin0);
+ASSERT(b[52:52] = 0bin1);
+ASSERT(b[53:53] = 0bin1);
+% ASSERT(b[54:54] = 0bin0);
+ASSERT(b[55:55] = 0bin1);
+ASSERT(b[56:56] = 0bin1);
+% ASSERT(b[57:57] = 0bin0);
+% ASSERT(b[58:58] = 0bin0);
+ASSERT(b[59:59] = 0bin1);
+ASSERT(b[60:60] = 0bin1);
+% ASSERT(b[61:61] = 0bin0);
+% ASSERT(b[62:62] = 0bin0);
+ASSERT(b[63:63] = 0bin1);
+% ASSERT(b[64:64] = 0bin0);
+% ASSERT(b[65:65] = 0bin0);
+% ASSERT(b[66:66] = 0bin0);
+ASSERT(b[67:67] = 0bin1);
+ASSERT(b[68:68] = 0bin1);
+ASSERT(b[69:69] = 0bin1);
+% ASSERT(b[70:70] = 0bin0);
+% ASSERT(b[71:71] = 0bin0);
+ASSERT(b[72:72] = 0bin1);
+% ASSERT(b[73:73] = 0bin0);
+ASSERT(b[74:74] = 0bin1);
+% ASSERT(b[75:75] = 0bin0);
+% ASSERT(b[76:76] = 0bin0);
+ASSERT(b[77:77] = 0bin1);
+% ASSERT(b[78:78] = 0bin0);
+% ASSERT(b[79:79] = 0bin0);
+% ASSERT(b[80:80] = 0bin0);
+% ASSERT(b[81:81] = 0bin0);
+ASSERT(b[82:82] = 0bin1);
+ASSERT(b[83:83] = 0bin1);
+% ASSERT(b[84:84] = 0bin0);
+ASSERT(b[85:85] = 0bin1);
+% ASSERT(b[86:86] = 0bin0);
+% ASSERT(b[87:87] = 0bin0);
+ASSERT(b[88:88] = 0bin1);
+ASSERT(b[89:89] = 0bin1);
+% ASSERT(b[90:90] = 0bin0);
+ASSERT(b[91:91] = 0bin1);
+% ASSERT(b[92:92] = 0bin0);
+ASSERT(b[93:93] = 0bin1);
+ASSERT(b[94:94] = 0bin1);
+ASSERT(b[95:95] = 0bin1);
+ASSERT(b[96:96] = 0bin1);
+% ASSERT(b[97:97] = 0bin0);
+% ASSERT(b[98:98] = 0bin0);
+% ASSERT(b[99:99] = 0bin0);
+ASSERT(b[100:100] = 0bin1);
+% ASSERT(b[101:101] = 0bin0);
+ASSERT(b[102:102] = 0bin1);
+% ASSERT(b[103:103] = 0bin0);
+% ASSERT(b[104:104] = 0bin0);
+% ASSERT(b[105:105] = 0bin0);
+ASSERT(b[106:106] = 0bin1);
+% ASSERT(b[107:107] = 0bin0);
+% ASSERT(b[108:108] = 0bin0);
+ASSERT(b[109:109] = 0bin1);
+% ASSERT(b[110:110] = 0bin0);
+
+ASSERT(a[431:216] = 0hex000000000000000000000000000000000000000000000000000000);
+ASSERT(b[431:216] = 0hex000000000000000000000000000000000000000000000000000000);
+
+%ASSERT(b[432:217] = 0hex000000000000000000000000000000000000000000000000000000);
+
+ASSERT(c=0hex00000000000000000000000000000000000000000000000000000016ba81dd77ec5a06e6455f3ff229b23691ec41c536d7e2d4582285);
+
+QUERY(
+   NOT (
+     c=BVMULT(432,a,b)
+     AND
+     NOT
+     a=0hex000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001
+     AND 
+     NOT
+     b=0hex000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001
+     AND NOT
+     a=c
+     AND NOT
+     b=c
+     
+   )
+);
+
+COUNTEREXAMPLE;
+
+
+
+
+
+
+
diff --git a/tests/sample-smt-tests/miniTest18.smt b/tests/sample-smt-tests/miniTest18.smt
new file mode 100644
index 0000000..e493dc8
--- /dev/null
+++ b/tests/sample-smt-tests/miniTest18.smt
@@ -0,0 +1,248 @@
+(benchmark BenchmarkName.smt
+:logic QF_AUFBV
+:extrafuns ((myarray BitVec[32] BitVec[32]))
+:extrafuns ((mychar BitVec[32]))
+:extrafuns ((myindex BitVec[32]))
+
+; 
+; Verification formulas
+; 
+:extrafuns ((in_1L0_1L0_0 BitVec[4]))
+:extrafuns ((in_1L0 BitVec[4]))
+:extrafuns ((in_1L0_1L0_1 BitVec[4]))
+:assumption
+(= in_1L0_1L0_1 in_1L0)
+; bit rSp
+:extrafuns ((rSp_3L0_0 BitVec[1]))
+; bit rSk
+:extrafuns ((rSk_3L1_0 BitVec[1]))
+; 
+; Inlining :reverseSketch
+; 
+:extrafuns ((in_1L0_5L0_0 BitVec[4]))
+:extrafuns ((in_1L0_5L0_1 BitVec[4]))
+:assumption
+(= in_1L0_5L0_1 in_1L0_1L0_1)
+:extrafuns ((sk__out_1L1_5L1_0 BitVec[1]))
+; _out_1L1 = 0
+:extrafuns ((sk__out_1L1_5L1_1 BitVec[1]))
+:assumption
+(= sk__out_1L1_5L1_1 bv0[1])
+; bit _has_out__3L0
+:extrafuns ((sk__has_out__3L0_7L0_0 BitVec[1]))
+; _has_out__3L0 = 0
+:extrafuns ((sk__has_out__3L0_7L0_1 BitVec[1]))
+:assumption
+(= sk__has_out__3L0_7L0_1 bv0[1])
+; bit[5] tmp_3L1
+:extrafuns ((tmp_3L1_7L1_0 BitVec[5]))
+; tmp_3L1 = ??:bit[5]:1
+:extrafuns ((tmp_3L1_7L1_1 BitVec[5]))
+:assumption
+(= tmp_3L1_7L1_1 bv0[5])
+; bit[2] tmp2_3L2
+:extrafuns ((tmp2_3L2_7L2_0 BitVec[2]))
+; tmp2_3L2 = ??:bit[2]:1
+:extrafuns ((tmp2_3L2_7L2_1 BitVec[2]))
+:assumption
+(= tmp2_3L2_7L2_1 bv0[2])
+; int lll_3L3
+:extrafuns ((lll_3L3_7L3_0 BitVec[5]))
+; lll_3L3 = ((int)tmp2_3L2)
+:extrafuns ((lll_3L3_7L3_1 BitVec[5]))
+:assumption
+(= lll_3L3_7L3_1 (concat bv0[3] tmp2_3L2_7L2_1))
+; int ttt_3L4
+:extrafuns ((ttt_3L4_7L4_0 BitVec[5]))
+; bit[5] __sa0
+:extrafuns ((sk___sa0_7L5_0 BitVec[5]))
+; __sa0 = tmp_3L1
+:extrafuns ((sk___sa0_7L5_1 BitVec[5]))
+:assumption
+(= sk___sa0_7L5_1 tmp_3L1_7L1_1)
+; bit[5] __sa1
+:extrafuns ((sk___sa1_7L6_0 BitVec[5]))
+; __sa1 = (__sa0)>>(lll_3L3)
+:extrafuns ((sk___sa1_7L6_1 BitVec[5]))
+:assumption
+(= sk___sa1_7L6_1 (ite		(= lll_3L3_7L3_1 bv0[5])
+	sk___sa0_7L5_1
+	(ite		(= lll_3L3_7L3_1 bv1[5])
+	(bvlshr sk___sa0_7L5_1 bv1[5])
+	(ite		(= lll_3L3_7L3_1 bv2[5])
+	(bvlshr sk___sa0_7L5_1 bv2[5])
+	(ite		(= lll_3L3_7L3_1 bv3[5])
+	(bvlshr sk___sa0_7L5_1 bv3[5])
+	(ite		(= lll_3L3_7L3_1 bv4[5])
+	(bvlshr sk___sa0_7L5_1 bv4[5])
+	(ite		(= lll_3L3_7L3_1 bv5[5])
+	(bvlshr sk___sa0_7L5_1 bv5[5])
+	(ite		(= lll_3L3_7L3_1 bv6[5])
+	(bvlshr sk___sa0_7L5_1 bv6[5])
+	(ite		(= lll_3L3_7L3_1 bv7[5])
+	(bvlshr sk___sa0_7L5_1 bv7[5])
+	(ite		(= lll_3L3_7L3_1 bv8[5])
+	(bvlshr sk___sa0_7L5_1 bv8[5])
+	(ite		(= lll_3L3_7L3_1 bv9[5])
+	(bvlshr sk___sa0_7L5_1 bv9[5])
+	(ite		(= lll_3L3_7L3_1 bv10[5])
+	(bvlshr sk___sa0_7L5_1 bv10[5])
+	(ite		(= lll_3L3_7L3_1 bv11[5])
+	(bvlshr sk___sa0_7L5_1 bv11[5])
+	(ite		(= lll_3L3_7L3_1 bv12[5])
+	(bvlshr sk___sa0_7L5_1 bv12[5])
+	(ite		(= lll_3L3_7L3_1 bv13[5])
+	(bvlshr sk___sa0_7L5_1 bv13[5])
+	(ite		(= lll_3L3_7L3_1 bv14[5])
+	(bvlshr sk___sa0_7L5_1 bv14[5])
+	(ite		(= lll_3L3_7L3_1 bv15[5])
+	(bvlshr sk___sa0_7L5_1 bv15[5])
+	(ite		(= lll_3L3_7L3_1 bv16[5])
+	(bvlshr sk___sa0_7L5_1 bv16[5])
+	(ite		(= lll_3L3_7L3_1 bv17[5])
+	(bvlshr sk___sa0_7L5_1 bv17[5])
+	(ite		(= lll_3L3_7L3_1 bv18[5])
+	(bvlshr sk___sa0_7L5_1 bv18[5])
+	(ite		(= lll_3L3_7L3_1 bv19[5])
+	(bvlshr sk___sa0_7L5_1 bv19[5])
+	(ite		(= lll_3L3_7L3_1 bv20[5])
+	(bvlshr sk___sa0_7L5_1 bv20[5])
+	(ite		(= lll_3L3_7L3_1 bv21[5])
+	(bvlshr sk___sa0_7L5_1 bv21[5])
+	(ite		(= lll_3L3_7L3_1 bv22[5])
+	(bvlshr sk___sa0_7L5_1 bv22[5])
+	(ite		(= lll_3L3_7L3_1 bv23[5])
+	(bvlshr sk___sa0_7L5_1 bv23[5])
+	(ite		(= lll_3L3_7L3_1 bv24[5])
+	(bvlshr sk___sa0_7L5_1 bv24[5])
+	(ite		(= lll_3L3_7L3_1 bv25[5])
+	(bvlshr sk___sa0_7L5_1 bv25[5])
+	(ite		(= lll_3L3_7L3_1 bv26[5])
+	(bvlshr sk___sa0_7L5_1 bv26[5])
+	(ite		(= lll_3L3_7L3_1 bv27[5])
+	(bvlshr sk___sa0_7L5_1 bv27[5])
+	(ite		(= lll_3L3_7L3_1 bv28[5])
+	(bvlshr sk___sa0_7L5_1 bv28[5])
+	(ite		(= lll_3L3_7L3_1 bv29[5])
+	(bvlshr sk___sa0_7L5_1 bv29[5])
+	(ite		(= lll_3L3_7L3_1 bv30[5])
+	(bvlshr sk___sa0_7L5_1 bv30[5])
+	(ite		(= lll_3L3_7L3_1 bv31[5])
+	(bvlshr sk___sa0_7L5_1 bv31[5])
+	(bvlshr sk___sa0_7L5_1 bv32[5])
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+))
+; ttt_3L4 = ((int)__sa1)
+:extrafuns ((ttt_3L4_7L4_1 BitVec[5]))
+:assumption
+(= ttt_3L4_7L4_1 sk___sa1_7L6_1)
+; int _pac2
+:extrafuns ((sk__pac2_9L0_0 BitVec[5]))
+; _pac2 = ttt_3L4
+:extrafuns ((sk__pac2_9L0_1 BitVec[5]))
+:assumption
+(= sk__pac2_9L0_1 ttt_3L4_7L4_1)
+; _out_1L1 = in_1L0[_pac2]
+:extrafuns ((rawArracTmp0_0 BitVec[1]))
+:extrafuns ((rawArracTmp0_1 BitVec[1]))
+:assumption
+(= rawArracTmp0_1 (ite		(= sk__pac2_9L0_1 bv0[5])
+	(extract[0:0] in_1L0_5L0_1)
+	(ite		(= sk__pac2_9L0_1 bv1[5])
+	(extract[1:1] in_1L0_5L0_1)
+	(ite		(= sk__pac2_9L0_1 bv2[5])
+	(extract[2:2] in_1L0_5L0_1)
+	(extract[3:3] in_1L0_5L0_1)
+)
+)
+))
+:extrafuns ((sk__out_1L1_5L1_2 BitVec[1]))
+:assumption
+(= sk__out_1L1_5L1_2 rawArracTmp0_1)
+; _has_out__3L0 = 1
+:extrafuns ((sk__has_out__3L0_7L0_2 BitVec[1]))
+:assumption
+(= sk__has_out__3L0_7L0_2 bv1[1])
+:extrafuns ((rSk_3L1_1 BitVec[1]))
+:assumption
+(= rSk_3L1_1 sk__out_1L1_5L1_2)
+; 
+; Done inlining :reverseSketch
+; 
+; 
+; Inlining :reverse
+; 
+:extrafuns ((in_5L2_11L0_0 BitVec[4]))
+:extrafuns ((in_5L2_11L0_1 BitVec[4]))
+:assumption
+(= in_5L2_11L0_1 in_1L0_1L0_1)
+:extrafuns ((sk__out_5L2_11L1_0 BitVec[1]))
+; _out_5L2 = 0
+:extrafuns ((sk__out_5L2_11L1_1 BitVec[1]))
+:assumption
+(= sk__out_5L2_11L1_1 bv0[1])
+; bit _has_out__7L0
+:extrafuns ((sk__has_out__7L0_13L0_0 BitVec[1]))
+; _has_out__7L0 = 0
+:extrafuns ((sk__has_out__7L0_13L0_1 BitVec[1]))
+:assumption
+(= sk__has_out__7L0_13L0_1 bv0[1])
+; int _pac3
+:extrafuns ((sk__pac3_14L0_0 BitVec[5]))
+; _pac3 = 2
+:extrafuns ((sk__pac3_14L0_1 BitVec[5]))
+:assumption
+(= sk__pac3_14L0_1 bv2[5])
+; _out_5L2 = in_5L2[_pac3]
+:extrafuns ((sk__out_5L2_11L1_2 BitVec[1]))
+:assumption
+(= sk__out_5L2_11L1_2 (extract[2:2] in_5L2_11L0_1))
+; _has_out__7L0 = 1
+:extrafuns ((sk__has_out__7L0_13L0_2 BitVec[1]))
+:assumption
+(= sk__has_out__7L0_13L0_2 bv1[1])
+:extrafuns ((rSp_3L0_1 BitVec[1]))
+:assumption
+(= rSp_3L0_1 sk__out_5L2_11L1_2)
+; 
+; Done inlining :reverse
+; 
+; 
+; Correctness Conditions
+; 
+:assumption
+(or		(not (bvslt ttt_3L4_7L4_1 bv4[5]))
+	(not (and (bvsge sk__pac2_9L0_1 bv0[5]) (bvslt sk__pac2_9L0_1 bv4[5])))
+	(not (= rSp_3L0_1 rSk_3L1_1))
+)
+)