added some more crypto examples

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

diff --git a/tests/crypto-tests/t4.stp b/tests/crypto-tests/t4.stp
new file mode 100644 (file)
index 0000000..76a40ed
--- /dev/null
+++ b/tests/crypto-tests/t4.stp
@@ -0,0 +1,131 @@
+
+a,b,c,x,y : BITVECTOR(216);
+
+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);
+
+QUERY(
+   NOT (
+     c=BVMULT(216,a,b)
+     AND
+     c=0hex16ba81dd77ec5a06e6455f3ff229b23691ec41c536d7e2d4582285
+     AND
+     NOT
+     a=0hex000000000000000000000000000000000000000000000000000001
+     AND 
+     NOT
+     b=0hex000000000000000000000000000000000000000000000000000001
+     AND NOT
+     a=c
+     AND NOT
+     b=c
+     AND NOT
+     BVGT(b,y)
+     
+   )
+);
+
+COUNTEREXAMPLE;
+

diff --git a/tests/crypto-tests/t4_flat.stp b/tests/crypto-tests/t4_flat.stp
new file mode 100644 (file)
index 0000000..3421bae
--- /dev/null
+++ b/tests/crypto-tests/t4_flat.stp
@@ -0,0 +1,134 @@
+
+a,b,c,x,y : BITVECTOR(432);
+
+
+
+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(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;
+