Fix. unit_test script was not working. Adds another test.

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

diff --git a/unit_test/bvmul_minus.smt2 b/unit_test/bvmul_minus.smt2
new file mode 100644 (file)
index 0000000..7d2cfa6
--- /dev/null
+++ b/unit_test/bvmul_minus.smt2
@@ -0,0 +1,23 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status unsat)
+(declare-fun x () (_ BitVec 8))
+(declare-fun y () (_ BitVec 8))
+
+
+
+
+; This is always true. 
+(assert 
+        (not (= 
+               (bvneg (bvmul (bvneg x) (bvneg y) ))
+               (bvneg (bvmul  y x ))
+               
+       ))
+)
+
+
+(check-sat)
+(exit)
+

diff --git a/unit_test/unit_test.sh b/unit_test/unit_test.sh
index ba04404b3c38864479484d5d548d434c17de7f3f..16c7c0fe077deace2ffdae9b9f980047f43b48be 100755 (executable)
--- a/unit_test/unit_test.sh
+++ b/unit_test/unit_test.sh
@@ -1,15 +1,17 @@
 #!/bin/bash     
 
-#Each file should be simplified down to either true or false, so the CNF generated should
-#be very small if simplifications are working as they should.
+#Each input should be simplified down to either true or false.
+#We no longer generate a CNF for trivially true/false instances,
+#so there should be no CNF generated for these.
+
 
 rm -f output_*.cnf
 
 files=`ls -1 -S *.smt2 *.smt`
 for f in $files; do
        stp --output-CNF $f
-       cnf=`cat output_*.cnf  | grep -v "^c" | grep -v "^$" |  wc -l`
-       if [ $cnf -gt 3 ] ; then
+       #cnf=`cat output_*.cnf  | grep -v "^c" | grep -v "^$" |  wc -l`
+       if [ -e output_0.cnf ] ; then
                echo --fail $f
                exit 10
        fi