removed a broken test

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

diff --git a/tests/sample-smt-tests/miniTest18.smt b/tests/sample-smt-tests/miniTest18.smt
deleted file mode 100644 (file)
index e493dc8..0000000
--- a/tests/sample-smt-tests/miniTest18.smt
+++ /dev/null
@@ -1,248 +0,0 @@
-(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