From e744f086684413a4cefa1ee713bf23047161c63a Mon Sep 17 00:00:00 2001
From: aqjune <aqjune@gmail.com>
Date: Fri, 1 Feb 2019 10:37:43 +0900
Subject: [PATCH] Update test scripts

---
 check_diff.py   | 6 +++---
 run-alive.sh    | 3 +--
 run-irtest.sh   | 2 +-
 run-proptest.sh | 0
 4 files changed, 5 insertions(+), 6 deletions(-)
 mode change 100644 => 100755 run-alive.sh
 mode change 100644 => 100755 run-proptest.sh

diff --git a/check_diff.py b/check_diff.py
index 28bde5e..243c5d0 100644
--- a/check_diff.py
+++ b/check_diff.py
@@ -4,11 +4,11 @@ import sys
 def matches(s1, s2):
 	s1 = s1.strip()
 	s2 = s2.strip()
-	if s1 != "sat" and s1 != "unsat":
+	if s1 != "Correct" and s1 != "Incorrect":
 		# Unknown output.
 		return 0
-	if (s1 == "unsat" and s2 == "Optimization is correct!") or \
-	   (s1 == "sat" and s2.startswith("ERROR:")):
+	if (s1 == "Correct" and s2 == "Optimization is correct!") or \
+	   (s1 == "Incorrect" and s2.startswith("ERROR:")):
 		# Correct.
 		return 1
 	# Incorrect!
diff --git a/run-alive.sh b/run-alive.sh
old mode 100644
new mode 100755
index 7781e3a..c580b42
--- a/run-alive.sh
+++ b/run-alive.sh
@@ -2,8 +2,7 @@ for i in "inputs/alive/instcombine" "inputs/alive/unit"; do
 	echo "Running ${i}/*.opt .."
 	find ${i} -name "opt*" -print0 | sort -z | xargs --null cat > ${i}/all.opt
 	lean -q --run src/main.lean -verifyopt ${i}/all.opt > output.txt
-	grep -E '^sat$|^unsat$' output.txt > output_summarized.txt
-	python3 check_diff.py output_summarized.txt ${i}/answ.txt
+	python3 check_diff.py output.txt ${i}/answ.txt
 	rm ${i}/all.opt
 	echo
 done
diff --git a/run-irtest.sh b/run-irtest.sh
index cdb3b79..a73aa4c 100755
--- a/run-irtest.sh
+++ b/run-irtest.sh
@@ -1,5 +1,5 @@
 # of testing
-n=10000
+n=5000
 # clang path
 clang=~/clang-7.0.1/bin/clang
 # verbosity, replace n with y if want the script to be verbose
diff --git a/run-proptest.sh b/run-proptest.sh
old mode 100644
new mode 100755