From 23f5724bc107d1bd84c58e583ac75d59e37e681d Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 12 Jul 2011 07:04:35 +0000
Subject: [PATCH] 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
---
 unit_test/bvmul_minus.smt2 | 23 +++++++++++++++++++++++
 unit_test/unit_test.sh     | 10 ++++++----
 2 files changed, 29 insertions(+), 4 deletions(-)
 create mode 100644 unit_test/bvmul_minus.smt2

diff --git a/unit_test/bvmul_minus.smt2 b/unit_test/bvmul_minus.smt2
new file mode 100644
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 ba04404..16c7c0f 100755
--- 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
-- 
2.47.3