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 (file)
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 (file)
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 (file)
index 0000000..e493dc8
--- /dev/null
+++ b/tests/sample-smt-tests/miniTest18.smt
@@ -0,0 +1,248 @@
+(benchmark BenchmarkName.smt\r
+:logic QF_AUFBV\r
+:extrafuns ((myarray BitVec[32] BitVec[32]))\r
+:extrafuns ((mychar BitVec[32]))\r
+:extrafuns ((myindex BitVec[32]))\r
+\r
+; \r
+; Verification formulas\r
+; \r
+:extrafuns ((in_1L0_1L0_0 BitVec[4]))\r
+:extrafuns ((in_1L0 BitVec[4]))\r
+:extrafuns ((in_1L0_1L0_1 BitVec[4]))\r
+:assumption\r
+(= in_1L0_1L0_1 in_1L0)\r
+; bit rSp\r
+:extrafuns ((rSp_3L0_0 BitVec[1]))\r
+; bit rSk\r
+:extrafuns ((rSk_3L1_0 BitVec[1]))\r
+; \r
+; Inlining :reverseSketch\r
+; \r
+:extrafuns ((in_1L0_5L0_0 BitVec[4]))\r
+:extrafuns ((in_1L0_5L0_1 BitVec[4]))\r
+:assumption\r
+(= in_1L0_5L0_1 in_1L0_1L0_1)\r
+:extrafuns ((sk__out_1L1_5L1_0 BitVec[1]))\r
+; _out_1L1 = 0\r
+:extrafuns ((sk__out_1L1_5L1_1 BitVec[1]))\r
+:assumption\r
+(= sk__out_1L1_5L1_1 bv0[1])\r
+; bit _has_out__3L0\r
+:extrafuns ((sk__has_out__3L0_7L0_0 BitVec[1]))\r
+; _has_out__3L0 = 0\r
+:extrafuns ((sk__has_out__3L0_7L0_1 BitVec[1]))\r
+:assumption\r
+(= sk__has_out__3L0_7L0_1 bv0[1])\r
+; bit[5] tmp_3L1\r
+:extrafuns ((tmp_3L1_7L1_0 BitVec[5]))\r
+; tmp_3L1 = ??:bit[5]:1\r
+:extrafuns ((tmp_3L1_7L1_1 BitVec[5]))\r
+:assumption\r
+(= tmp_3L1_7L1_1 bv0[5])\r
+; bit[2] tmp2_3L2\r
+:extrafuns ((tmp2_3L2_7L2_0 BitVec[2]))\r
+; tmp2_3L2 = ??:bit[2]:1\r
+:extrafuns ((tmp2_3L2_7L2_1 BitVec[2]))\r
+:assumption\r
+(= tmp2_3L2_7L2_1 bv0[2])\r
+; int lll_3L3\r
+:extrafuns ((lll_3L3_7L3_0 BitVec[5]))\r
+; lll_3L3 = ((int)tmp2_3L2)\r
+:extrafuns ((lll_3L3_7L3_1 BitVec[5]))\r
+:assumption\r
+(= lll_3L3_7L3_1 (concat bv0[3] tmp2_3L2_7L2_1))\r
+; int ttt_3L4\r
+:extrafuns ((ttt_3L4_7L4_0 BitVec[5]))\r
+; bit[5] __sa0\r
+:extrafuns ((sk___sa0_7L5_0 BitVec[5]))\r
+; __sa0 = tmp_3L1\r
+:extrafuns ((sk___sa0_7L5_1 BitVec[5]))\r
+:assumption\r
+(= sk___sa0_7L5_1 tmp_3L1_7L1_1)\r
+; bit[5] __sa1\r
+:extrafuns ((sk___sa1_7L6_0 BitVec[5]))\r
+; __sa1 = (__sa0)>>(lll_3L3)\r
+:extrafuns ((sk___sa1_7L6_1 BitVec[5]))\r
+:assumption\r
+(= sk___sa1_7L6_1 (ite         (= lll_3L3_7L3_1 bv0[5])\r
+       sk___sa0_7L5_1\r
+       (ite            (= lll_3L3_7L3_1 bv1[5])\r
+       (bvlshr sk___sa0_7L5_1 bv1[5])\r
+       (ite            (= lll_3L3_7L3_1 bv2[5])\r
+       (bvlshr sk___sa0_7L5_1 bv2[5])\r
+       (ite            (= lll_3L3_7L3_1 bv3[5])\r
+       (bvlshr sk___sa0_7L5_1 bv3[5])\r
+       (ite            (= lll_3L3_7L3_1 bv4[5])\r
+       (bvlshr sk___sa0_7L5_1 bv4[5])\r
+       (ite            (= lll_3L3_7L3_1 bv5[5])\r
+       (bvlshr sk___sa0_7L5_1 bv5[5])\r
+       (ite            (= lll_3L3_7L3_1 bv6[5])\r
+       (bvlshr sk___sa0_7L5_1 bv6[5])\r
+       (ite            (= lll_3L3_7L3_1 bv7[5])\r
+       (bvlshr sk___sa0_7L5_1 bv7[5])\r
+       (ite            (= lll_3L3_7L3_1 bv8[5])\r
+       (bvlshr sk___sa0_7L5_1 bv8[5])\r
+       (ite            (= lll_3L3_7L3_1 bv9[5])\r
+       (bvlshr sk___sa0_7L5_1 bv9[5])\r
+       (ite            (= lll_3L3_7L3_1 bv10[5])\r
+       (bvlshr sk___sa0_7L5_1 bv10[5])\r
+       (ite            (= lll_3L3_7L3_1 bv11[5])\r
+       (bvlshr sk___sa0_7L5_1 bv11[5])\r
+       (ite            (= lll_3L3_7L3_1 bv12[5])\r
+       (bvlshr sk___sa0_7L5_1 bv12[5])\r
+       (ite            (= lll_3L3_7L3_1 bv13[5])\r
+       (bvlshr sk___sa0_7L5_1 bv13[5])\r
+       (ite            (= lll_3L3_7L3_1 bv14[5])\r
+       (bvlshr sk___sa0_7L5_1 bv14[5])\r
+       (ite            (= lll_3L3_7L3_1 bv15[5])\r
+       (bvlshr sk___sa0_7L5_1 bv15[5])\r
+       (ite            (= lll_3L3_7L3_1 bv16[5])\r
+       (bvlshr sk___sa0_7L5_1 bv16[5])\r
+       (ite            (= lll_3L3_7L3_1 bv17[5])\r
+       (bvlshr sk___sa0_7L5_1 bv17[5])\r
+       (ite            (= lll_3L3_7L3_1 bv18[5])\r
+       (bvlshr sk___sa0_7L5_1 bv18[5])\r
+       (ite            (= lll_3L3_7L3_1 bv19[5])\r
+       (bvlshr sk___sa0_7L5_1 bv19[5])\r
+       (ite            (= lll_3L3_7L3_1 bv20[5])\r
+       (bvlshr sk___sa0_7L5_1 bv20[5])\r
+       (ite            (= lll_3L3_7L3_1 bv21[5])\r
+       (bvlshr sk___sa0_7L5_1 bv21[5])\r
+       (ite            (= lll_3L3_7L3_1 bv22[5])\r
+       (bvlshr sk___sa0_7L5_1 bv22[5])\r
+       (ite            (= lll_3L3_7L3_1 bv23[5])\r
+       (bvlshr sk___sa0_7L5_1 bv23[5])\r
+       (ite            (= lll_3L3_7L3_1 bv24[5])\r
+       (bvlshr sk___sa0_7L5_1 bv24[5])\r
+       (ite            (= lll_3L3_7L3_1 bv25[5])\r
+       (bvlshr sk___sa0_7L5_1 bv25[5])\r
+       (ite            (= lll_3L3_7L3_1 bv26[5])\r
+       (bvlshr sk___sa0_7L5_1 bv26[5])\r
+       (ite            (= lll_3L3_7L3_1 bv27[5])\r
+       (bvlshr sk___sa0_7L5_1 bv27[5])\r
+       (ite            (= lll_3L3_7L3_1 bv28[5])\r
+       (bvlshr sk___sa0_7L5_1 bv28[5])\r
+       (ite            (= lll_3L3_7L3_1 bv29[5])\r
+       (bvlshr sk___sa0_7L5_1 bv29[5])\r
+       (ite            (= lll_3L3_7L3_1 bv30[5])\r
+       (bvlshr sk___sa0_7L5_1 bv30[5])\r
+       (ite            (= lll_3L3_7L3_1 bv31[5])\r
+       (bvlshr sk___sa0_7L5_1 bv31[5])\r
+       (bvlshr sk___sa0_7L5_1 bv32[5])\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+)\r
+))\r
+; ttt_3L4 = ((int)__sa1)\r
+:extrafuns ((ttt_3L4_7L4_1 BitVec[5]))\r
+:assumption\r
+(= ttt_3L4_7L4_1 sk___sa1_7L6_1)\r
+; int _pac2\r
+:extrafuns ((sk__pac2_9L0_0 BitVec[5]))\r
+; _pac2 = ttt_3L4\r
+:extrafuns ((sk__pac2_9L0_1 BitVec[5]))\r
+:assumption\r
+(= sk__pac2_9L0_1 ttt_3L4_7L4_1)\r
+; _out_1L1 = in_1L0[_pac2]\r
+:extrafuns ((rawArracTmp0_0 BitVec[1]))\r
+:extrafuns ((rawArracTmp0_1 BitVec[1]))\r
+:assumption\r
+(= rawArracTmp0_1 (ite         (= sk__pac2_9L0_1 bv0[5])\r
+       (extract[0:0] in_1L0_5L0_1)\r
+       (ite            (= sk__pac2_9L0_1 bv1[5])\r
+       (extract[1:1] in_1L0_5L0_1)\r
+       (ite            (= sk__pac2_9L0_1 bv2[5])\r
+       (extract[2:2] in_1L0_5L0_1)\r
+       (extract[3:3] in_1L0_5L0_1)\r
+)\r
+)\r
+))\r
+:extrafuns ((sk__out_1L1_5L1_2 BitVec[1]))\r
+:assumption\r
+(= sk__out_1L1_5L1_2 rawArracTmp0_1)\r
+; _has_out__3L0 = 1\r
+:extrafuns ((sk__has_out__3L0_7L0_2 BitVec[1]))\r
+:assumption\r
+(= sk__has_out__3L0_7L0_2 bv1[1])\r
+:extrafuns ((rSk_3L1_1 BitVec[1]))\r
+:assumption\r
+(= rSk_3L1_1 sk__out_1L1_5L1_2)\r
+; \r
+; Done inlining :reverseSketch\r
+; \r
+; \r
+; Inlining :reverse\r
+; \r
+:extrafuns ((in_5L2_11L0_0 BitVec[4]))\r
+:extrafuns ((in_5L2_11L0_1 BitVec[4]))\r
+:assumption\r
+(= in_5L2_11L0_1 in_1L0_1L0_1)\r
+:extrafuns ((sk__out_5L2_11L1_0 BitVec[1]))\r
+; _out_5L2 = 0\r
+:extrafuns ((sk__out_5L2_11L1_1 BitVec[1]))\r
+:assumption\r
+(= sk__out_5L2_11L1_1 bv0[1])\r
+; bit _has_out__7L0\r
+:extrafuns ((sk__has_out__7L0_13L0_0 BitVec[1]))\r
+; _has_out__7L0 = 0\r
+:extrafuns ((sk__has_out__7L0_13L0_1 BitVec[1]))\r
+:assumption\r
+(= sk__has_out__7L0_13L0_1 bv0[1])\r
+; int _pac3\r
+:extrafuns ((sk__pac3_14L0_0 BitVec[5]))\r
+; _pac3 = 2\r
+:extrafuns ((sk__pac3_14L0_1 BitVec[5]))\r
+:assumption\r
+(= sk__pac3_14L0_1 bv2[5])\r
+; _out_5L2 = in_5L2[_pac3]\r
+:extrafuns ((sk__out_5L2_11L1_2 BitVec[1]))\r
+:assumption\r
+(= sk__out_5L2_11L1_2 (extract[2:2] in_5L2_11L0_1))\r
+; _has_out__7L0 = 1\r
+:extrafuns ((sk__has_out__7L0_13L0_2 BitVec[1]))\r
+:assumption\r
+(= sk__has_out__7L0_13L0_2 bv1[1])\r
+:extrafuns ((rSp_3L0_1 BitVec[1]))\r
+:assumption\r
+(= rSp_3L0_1 sk__out_5L2_11L1_2)\r
+; \r
+; Done inlining :reverse\r
+; \r
+; \r
+; Correctness Conditions\r
+; \r
+:assumption\r
+(or            (not (bvslt ttt_3L4_7L4_1 bv4[5]))\r
+       (not (and (bvsge sk__pac2_9L0_1 bv0[5]) (bvslt sk__pac2_9L0_1 bv4[5])))\r
+       (not (= rSp_3L0_1 rSk_3L1_1))\r
+)\r
+)\r