actually pushing this copy out for realase...

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

diff --git a/Makefile.in b/Makefile.in
index 169adbc03b91a11b50839d302e1dfb22c83dc082..1438bce893ca0b57e721f6fabb8ef111ea9f33e1 100644 (file)
--- a/Makefile.in
+++ b/Makefile.in
@@ -51,8 +51,8 @@ clean:
        rm -rf bin/*~
        rm -rf bin/stp
        rm -rf *.log
-       @#rm -rf Makefile
-       @#rm -rf config.info
+       #rm -rf Makefile
+       #rm -rf config.info
        rm -f TAGS
        $(MAKE) clean -C AST
        $(MAKE) clean -C sat/core
@@ -117,7 +117,6 @@ regressbigarray:
 
 .PHONY: regressall
 regressall:
-       $(MAKE) install
        $(MAKE) regress
 
 GRIND_LOG = `date +%Y-%m-%d`"-grind.log"

diff --git a/bin/run_tests b/bin/run_tests
index 40490aff87eb8b0abaedfc18f6c4f17a5315e170..5571e658c657b1a26524d3a312b7e5d70040db29 100755 (executable)
--- a/bin/run_tests
+++ b/bin/run_tests
@@ -84,7 +84,7 @@ my %optionsDefault = ("level" => 4,
 my %options = ();
 # The list of testcases to run
 #
-my @testcases = "bigarray-test";
+my @testcases = "sample-tests";
 # Temporary array for STP options
 my @stpOptions = ();
 # State is either "own" or "stp", meaning that we're reading either

diff --git a/sample-tests/egt-1899.cvc b/sample-tests/egt-1899.cvc
new file mode 100644 (file)
index 0000000..2cb952a
--- /dev/null
+++ b/sample-tests/egt-1899.cvc
@@ -0,0 +1,217 @@
+%% Regression level = 2
+%% Result = Valid
+%% Language = presentation
+%START----------------------------------
+packet: ARRAY BITVECTOR(32) OF BITVECTOR(8);
+%----------------------------------------------------
+ASSERT ((0bin000000000000000000000000 @ packet[0bin00000000000000000000000011110000]) 
+ = 0bin00000000000000000000000000110101);
+ASSERT NOT NOT ((0bin000000000000000000000000 @ 
+          0bin00000000) = (0bin000000000000000000000000 
+                           @ packet[0bin00000000000000000000000000011100]));
+ASSERT NOT ((0bin000000000000000000000000 @ 
+      0bin00000000) = (0bin000000000000000000000000 
+                       @ packet[0bin00000000000000000000000000011101]));
+ASSERT ((0bin000000000000000000000000 @ packet[0bin00000000000000000000000011110010]) 
+ = 0bin00000000000000000000000000000001);
+ASSERT NOT ((0bin000000000000000000000000 @ 
+      packet[BVPLUS(32, 0bin00000000000000000000000011110010, 
+                    (0bin000000000000000000000000 
+                     @ packet[0bin00000000000000000000000011110001]))]) 
+     = 0bin00000000000000000000000000110010);
+ASSERT NOT ((0bin000000000000000000000000 @ 
+      packet[BVPLUS(32, 0bin00000000000000000000000011110010, 
+                    (0bin000000000000000000000000 
+                     @ packet[0bin00000000000000000000000011110001]))]) 
+     = 0bin00000000000000000000000000000000);
+ASSERT NOT ((0bin000000000000000000000000 @ 
+      packet[BVPLUS(32, 0bin00000000000000000000000011110010, 
+                    (0bin000000000000000000000000 
+                     @ packet[0bin00000000000000000000000011110001]))]) 
+     = 0bin00000000000000000000000000110100);
+ASSERT NOT ((0bin000000000000000000000000 @ 
+      packet[BVPLUS(32, 0bin00000000000000000000000011110010, 
+                    (0bin000000000000000000000000 
+                     @ packet[0bin00000000000000000000000011110001]))]) 
+     = 0bin00000000000000000000000011111111);
+ASSERT (LET cvcl_0 = (0bin000000000000000000000000 
+               @ packet[0bin00000000000000000000000011110001])
+ IN NOT SBVLE(0bin00000000000000000000000100110100
+              ,BVPLUS(32, BVPLUS(32, 0bin00000000000000000000000000000000, 
+                                 BVPLUS(32, cvcl_0, 0bin00000000000000000000000000000010)), 
+                      BVPLUS(32, (0bin000000000000000000000000 
+                                  @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, 
+                                                  cvcl_0)]), 
+                             0bin00000000000000000000000000000010))));
+ASSERT (LET cvcl_0 = (0bin000000000000000000000000 
+               @ packet[0bin00000000000000000000000011110001])
+ IN NOT ((0bin000000000000000000000000 @ 
+          packet[BVPLUS(32, 0bin00000000000000000000000011110100, 
+                        cvcl_0, (0bin000000000000000000000000 
+                                 @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, 
+                                                 cvcl_0)]))]) 
+         = 0bin00000000000000000000000000110010));
+ASSERT (LET cvcl_0 = (0bin000000000000000000000000 
+               @ packet[0bin00000000000000000000000011110001])
+ IN ((0bin000000000000000000000000 @ 
+      packet[BVPLUS(32, 0bin00000000000000000000000011110100, 
+                    cvcl_0, (0bin000000000000000000000000 
+                             @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, 
+                                             cvcl_0)]))]) 
+     = 0bin00000000000000000000000000000000));
+ASSERT (LET cvcl_0 = (0bin000000000000000000000000 
+               @ packet[0bin00000000000000000000000011110001])
+ IN NOT SBVLE(0bin00000000000000000000000100110100
+              ,BVPLUS(32, BVPLUS(32, BVPLUS(32, 0bin00000000000000000000000000000000, 
+                                            BVPLUS(32, cvcl_0, 0bin00000000000000000000000000000010)), 
+                                 BVPLUS(32, (0bin000000000000000000000000 
+                                             @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, 
+                                                             cvcl_0)]), 
+                                        0bin00000000000000000000000000000010)), 
+                      0bin00000000000000000000000000000001)));
+ASSERT (LET cvcl_0 = (0bin000000000000000000000000 
+               @ packet[0bin00000000000000000000000011110001])
+ IN NOT ((0bin000000000000000000000000 @ 
+          packet[BVPLUS(32, 0bin00000000000000000000000011110101, 
+                        cvcl_0, (0bin000000000000000000000000 
+                                 @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, 
+                                                 cvcl_0)]))]) 
+         = 0bin00000000000000000000000000110010));
+ASSERT (LET cvcl_0 = (0bin000000000000000000000000 
+               @ packet[0bin00000000000000000000000011110001])
+ IN NOT ((0bin000000000000000000000000 @ 
+          packet[BVPLUS(32, 0bin00000000000000000000000011110101, 
+                        cvcl_0, (0bin000000000000000000000000 
+                                 @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, 
+                                                 cvcl_0)]))]) 
+         = 0bin00000000000000000000000000000000));
+ASSERT (LET cvcl_0 = (0bin000000000000000000000000 
+               @ packet[0bin00000000000000000000000011110001])
+ IN NOT ((0bin000000000000000000000000 @ 
+          packet[BVPLUS(32, 0bin00000000000000000000000011110101, 
+                        cvcl_0, (0bin000000000000000000000000 
+                                 @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, 
+                                                 cvcl_0)]))]) 
+         = 0bin00000000000000000000000000110100));
+ASSERT (LET cvcl_0 = (0bin000000000000000000000000 
+               @ packet[0bin00000000000000000000000011110001])
+ IN NOT ((0bin000000000000000000000000 @ 
+          packet[BVPLUS(32, 0bin00000000000000000000000011110101, 
+                        cvcl_0, (0bin000000000000000000000000 
+                                 @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, 
+                                                 cvcl_0)]))]) 
+         = 0bin00000000000000000000000011111111));
+ASSERT (LET cvcl_0 = (0bin000000000000000000000000 
+               @ packet[0bin00000000000000000000000011110001]),
+     cvcl_1 = BVPLUS(32, 0bin00000000000000000000000011110110, 
+                     cvcl_0, (0bin000000000000000000000000 
+                              @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, 
+                                              cvcl_0)]))
+ IN (BVLE(0bin00000000000000000000000000000000
+          ,cvcl_1) AND BVLE(cvcl_1,0bin00000000000000000000001000100011)));
+ASSERT (LET cvcl_0 = (0bin000000000000000000000000 
+               @ packet[0bin00000000000000000000000011110001]),
+     cvcl_1 = (0bin000000000000000000000000 
+               @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, 
+                               cvcl_0)])
+ IN NOT SBVLE(0bin00000000000000000000000100110100
+              ,BVPLUS(32, BVPLUS(32, BVPLUS(32, BVPLUS(32, 0bin00000000000000000000000000000000, 
+                                                       BVPLUS(32, cvcl_0, 0bin00000000000000000000000000000010)), 
+                                            BVPLUS(32, cvcl_1, 0bin00000000000000000000000000000010)), 
+                                 0bin00000000000000000000000000000001), 
+                      BVPLUS(32, (0bin000000000000000000000000 
+                                  @ packet[BVPLUS(32, 0bin00000000000000000000000011110110, 
+                                                  cvcl_0, cvcl_1)]), 
+                             0bin00000000000000000000000000000010))));
+ASSERT (LET cvcl_0 = (0bin000000000000000000000000 
+               @ packet[0bin00000000000000000000000011110001]),
+     cvcl_1 = (0bin000000000000000000000000 
+               @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, 
+                               cvcl_0)])
+ IN NOT ((0bin000000000000000000000000 @ 
+          packet[BVPLUS(32, 0bin00000000000000000000000011110111, 
+                        cvcl_0, cvcl_1, (0bin000000000000000000000000 
+                                         @ packet[BVPLUS(32, 0bin00000000000000000000000011110110, 
+                                                         cvcl_0, cvcl_1)]))]) 
+         = 0bin00000000000000000000000000110010));
+ASSERT (LET cvcl_0 = (0bin000000000000000000000000 
+               @ packet[0bin00000000000000000000000011110001]),
+     cvcl_1 = (0bin000000000000000000000000 
+               @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, 
+                               cvcl_0)])
+ IN ((0bin000000000000000000000000 @ 
+      packet[BVPLUS(32, 0bin00000000000000000000000011110111, 
+                    cvcl_0, cvcl_1, (0bin000000000000000000000000 
+                                     @ packet[BVPLUS(32, 0bin00000000000000000000000011110110, 
+                                                     cvcl_0, cvcl_1)]))]) 
+     = 0bin00000000000000000000000000000000));
+ASSERT (LET cvcl_0 = (0bin000000000000000000000000 
+               @ packet[0bin00000000000000000000000011110001]),
+     cvcl_1 = (0bin000000000000000000000000 
+               @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, 
+                               cvcl_0)])
+ IN NOT SBVLE(0bin00000000000000000000000100110100
+              ,BVPLUS(32, BVPLUS(32, BVPLUS(32, BVPLUS(32, BVPLUS(32, 0bin00000000000000000000000000000000, 
+                                                                  BVPLUS(32, cvcl_0, 0bin00000000000000000000000000000010)), 
+                                                       BVPLUS(32, cvcl_1, 0bin00000000000000000000000000000010)), 
+                                            0bin00000000000000000000000000000001), 
+                                 BVPLUS(32, (0bin000000000000000000000000 
+                                             @ packet[BVPLUS(32, 0bin00000000000000000000000011110110, 
+                                                             cvcl_0, cvcl_1)]), 
+                                        0bin00000000000000000000000000000010)), 
+                      0bin00000000000000000000000000000001)));
+ASSERT (LET cvcl_0 = (0bin000000000000000000000000 
+               @ packet[0bin00000000000000000000000011110001]),
+     cvcl_1 = (0bin000000000000000000000000 
+               @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, 
+                               cvcl_0)])
+ IN NOT ((0bin000000000000000000000000 @ 
+          packet[BVPLUS(32, 0bin00000000000000000000000011111000, 
+                        cvcl_0, cvcl_1, (0bin000000000000000000000000 
+                                         @ packet[BVPLUS(32, 0bin00000000000000000000000011110110, 
+                                                         cvcl_0, cvcl_1)]))]) 
+         = 0bin00000000000000000000000000110010));
+ASSERT (LET cvcl_0 = (0bin000000000000000000000000 
+               @ packet[0bin00000000000000000000000011110001]),
+     cvcl_1 = (0bin000000000000000000000000 
+               @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, 
+                               cvcl_0)])
+ IN NOT ((0bin000000000000000000000000 @ 
+          packet[BVPLUS(32, 0bin00000000000000000000000011111000, 
+                        cvcl_0, cvcl_1, (0bin000000000000000000000000 
+                                         @ packet[BVPLUS(32, 0bin00000000000000000000000011110110, 
+                                                         cvcl_0, cvcl_1)]))]) 
+         = 0bin00000000000000000000000000000000));
+ASSERT (LET cvcl_0 = (0bin000000000000000000000000 
+               @ packet[0bin00000000000000000000000011110001]),
+     cvcl_1 = (0bin000000000000000000000000 
+               @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, 
+                               cvcl_0)])
+ IN ((0bin000000000000000000000000 @ 
+      packet[BVPLUS(32, 0bin00000000000000000000000011111000, 
+                    cvcl_0, cvcl_1, (0bin000000000000000000000000 
+                                     @ packet[BVPLUS(32, 0bin00000000000000000000000011110110, 
+                                                     cvcl_0, cvcl_1)]))]) 
+     = 0bin00000000000000000000000000110100));
+ASSERT (LET cvcl_0 = (0bin000000000000000000000000 
+               @ packet[0bin00000000000000000000000011110001]),
+     cvcl_1 = (0bin000000000000000000000000 
+               @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, 
+                               cvcl_0)])
+ IN SBVLE(0bin00000000000000000000000100110100
+          ,BVPLUS(32, BVPLUS(32, BVPLUS(32, BVPLUS(32, BVPLUS(32, BVPLUS(32, BVPLUS(32, 0bin00000000000000000000000000000000, 
+                                                                                    BVPLUS(32, cvcl_0, 0bin00000000000000000000000000000010)), 
+                                                                         BVPLUS(32, cvcl_1, 0bin00000000000000000000000000000010)), 
+                                                              0bin00000000000000000000000000000001), 
+                                                   BVPLUS(32, (0bin000000000000000000000000 
+                                                               @ packet[BVPLUS(32, 0bin00000000000000000000000011110110, 
+                                                                               cvcl_0, cvcl_1)]), 
+                                                          0bin00000000000000000000000000000010)), 
+                                        0bin00000000000000000000000000000001), 
+                             0bin00000000000000000000000000000001), 
+                  (0bin000000000000000000000000 
+                   @ 0bin00000000))));
+QUERY NOT ((0bin000000000000000000000000 @ 
+      packet[0bin00000000000000000000000011110000]) 
+     = 0bin00000000000000000000000000110100);
+%END------------------------------------