added python scripts (work in unix and windows) for testing Z3 and CVC4 to many of the test suite dirs

13 files changed, 868 insertions, 2 deletions

diff --git a/Test/CollectBenchmarks.py b/Test/CollectBenchmarks.py
index d5c8a233..97e37ecc 100644..100755
--- a/Test/CollectBenchmarks.py
+++ b/Test/CollectBenchmarks.py
@@ -13,7 +13,8 @@ import zipfile;
 

 

 #PROVER_NAME = "smt"

-PROVER_NAME = "simplify"

+#PROVER_NAME = "simplify"

+PROVER_NAME = "cvc4"

 

 # constants

 # prefix of temporary files created by boogie

@@ -25,6 +26,7 @@ PREFIX_PGK = "boogie"
 # arguments to runtest so that boogie creates problem specifications

 BOOGIE_ARG0 = "/prover:blank /print:" + PREFIX_TMP + ".@TIME@.bpl /proverLog:" + PREFIX_TMP + ".@TIME@.simplify"

 BOOGIE_ARG1 = "/prover:smt /print:" + PREFIX_TMP + ".@TIME@.bpl /proverLog:" + PREFIX_TMP + ".@TIME@.jjsmt"

+BOOGIE_ARG2 = "/prover:cvc4 /print:" + PREFIX_TMP + ".@TIME@.bpl /proverLog:" + PREFIX_TMP + ".@TIME@.cvc4"

 

 # file containing the directories with tests

 TESTS_FILE = "alltests.txt"

@@ -51,10 +53,12 @@ def runtests(parameters):
      boogie_arg = BOOGIE_ARG0

   if PROVER_NAME == "smt":

      boogie_arg = BOOGIE_ARG1

+  if PROVER_NAME == "cvc4":

+     boogie_arg = BOOGIE_ARG2

   if os.name == "nt":

     command = "runtestall.bat "  + " ".join(parameters) + " " + boogie_arg

   else:

-    command = "./rtestall "  + " ".join(parameters) + " " + boogie_arg

+    command = "sh rtestall.sh "  + " ".join(parameters) + " " + boogie_arg

   

   print command

 

diff --git a/Test/houdini/runtest.py b/Test/houdini/runtest.py
new file mode 100755
index 00000000..89b38404
--- /dev/null
+++ b/Test/houdini/runtest.py
@@ -0,0 +1,72 @@
+#!/usr/bin/python

+

+# 2013 Pantazis Deligiannis

+#

+# runs the test cases of this directory

+

+import sys;

+import os;

+import getopt;

+

+MONO = "/usr/bin/mono "

+BOOGIE = "/Users/pantazis/workspace/boogie/Binaries/Boogie.exe "

+

+PROVER_OPTIONS_Z3 = "/nologo "

+PROVER_OPTIONS_CVC4 = "/proverOpt:SOLVER=cvc4 /nologo "

+

+# choose a parser

+opts, args = getopt.getopt(sys.argv[1:], "s:", ["solver="])

+solver = "Z3"

+for o, a in opts:

+  if o in ("-s", "--solver"):

+      if a == "cvc4":

+          solver = a

+

+# if the Output file exists remove it

+if os.path.exists("Output"):

+  os.remove("Output")

+

+# runs the given test

+def runtest(filename):

+  if solver == "cvc4":

+    if os.name == "nt":

+      command = BOOGIE + PROVER_OPTIONS_CVC4 + filename

+    else:

+	  command = MONO + BOOGIE + PROVER_OPTIONS_CVC4 + filename

+  else:

+    if os.name == "nt":

+      command = BOOGIE + PROVER_OPTIONS_Z3 + filename

+    else:

+	  command = MONO + BOOGIE + PROVER_OPTIONS_Z3 + filename

+  

+  print "===== Testing: " + filename

+  

+  if os.path.exists("Output"):

+    os.system(command + " >> Output")

+  else:

+    os.system(command + " > Output")

+

+files = ["houd1.bpl", "houd2.bpl", "houd3.bpl", "houd4.bpl", "houd5.bpl", "houd6.bpl", "houd7.bpl", "houd8.bpl", "houd9.bpl", "houd10.bpl", "houd11.bpl", "houd12.bpl"]

+

+for file in files:

+  os.system("echo >> Output")

+  os.system("echo -------------------- " + file + " -------------------- >> Output")

+  runtest("/noinfer /contractInfer /printAssignment " + file)

+

+files = ["test1.bpl", "test2.bpl", "test7.bpl", "test8.bpl", "test9.bpl", "test10.bpl"]

+

+for file in files:

+  os.system("echo . >> Output")

+  os.system("echo -------------------- " + file + " -------------------- >> Output")

+  runtest("/noinfer /contractInfer /printAssignment /inlineDepth:1 " + file)

+

+# compare the output with the expected answers

+test_file = open("Output").readlines()

+correct_file = open("Answer").readlines()

+

+for test, correct in zip(test_file, correct_file):

+    if test.strip(' \t\n\r') != correct.strip(' \t\n\r'):

+        print "\n===== " + os.getcwd().split(os.sep)[-1] + ": FAILED"

+        break

+else:

+    print "\n===== " + os.getcwd().split(os.sep)[-1] + ": PASSED"

diff --git a/Test/runtest.bat b/Test/runtest.bat
index 5b3d45ae..5b3d45ae 100644..100755
--- a/Test/runtest.bat
+++ b/Test/runtest.bat
diff --git a/Test/test0/runtest.py b/Test/test0/runtest.py
new file mode 100755
index 00000000..2b240203
--- /dev/null
+++ b/Test/test0/runtest.py
@@ -0,0 +1,99 @@
+#!/usr/bin/python

+

+# 2013 Pantazis Deligiannis

+#

+# runs the test cases of this directory

+

+import sys;

+import os;

+import getopt;

+

+MONO = "/usr/bin/mono "

+BOOGIE = "/Users/pantazis/workspace/boogie/Binaries/Boogie.exe "

+

+PROVER_OPTIONS_Z3 = "/nologo "

+PROVER_OPTIONS_CVC4 = "/proverOpt:SOLVER=cvc4 /nologo "

+

+# choose a parser

+opts, args = getopt.getopt(sys.argv[1:], "s:", ["solver="])

+solver = "Z3"

+for o, a in opts:

+  if o in ("-s", "--solver"):

+      if a == "cvc4":

+          solver = a

+

+# if the Output file exists remove it

+if os.path.exists("Output"):

+  os.remove("Output")

+

+# runs the given test

+def runtest(filename):

+  if solver == "cvc4":

+    if os.name == "nt":

+      command = BOOGIE + PROVER_OPTIONS_CVC4 + filename

+    else:

+	  command = MONO + BOOGIE + PROVER_OPTIONS_CVC4 + filename

+  else:

+    if os.name == "nt":

+      command = BOOGIE + PROVER_OPTIONS_Z3 + filename

+    else:

+	  command = MONO + BOOGIE + PROVER_OPTIONS_Z3 + filename

+  

+  print "===== Testing: " + filename

+  

+  if filename == "SeparateVerification0.bpl":

+    os.system("echo ----- SeparateVerification0.bpl >> Output")

+  elif filename == "SeparateVerification1.bpl SeparateVerification0.bpl":

+    os.system("echo ----- SeparateVerification1.bpl SeparateVerification0.bpl >> Output")

+  elif filename == "SeparateVerification0.bpl SeparateVerification0.bpl":

+    os.system("echo ----- SeparateVerification0.bpl SeparateVerification0.bpl >> Output")

+  elif filename == "SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl":

+    os.system("echo ----- SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl >> Output")

+  

+  if os.path.exists("Output"):

+    os.system(command + " >> Output")

+  else:

+    os.system(command + " > Output")

+

+#runtest("Prog0.bpl")

+#runtest("ModifiedBag.bpl")

+runtest("Triggers0.bpl")

+runtest("Triggers1.bpl")

+runtest("/printInstrumented PrettyPrint.bpl")

+runtest("Arrays0.bpl")

+runtest("Arrays1.bpl")

+runtest("Types0.bpl")

+runtest("Types1.bpl")

+runtest("WhereParsing.bpl")

+runtest("WhereParsing0.bpl")

+runtest("WhereParsing1.bpl")

+runtest("WhereParsing2.bpl")

+runtest("WhereResolution.bpl")

+runtest("BadLabels0.bpl")

+runtest("BadLabels1.bpl")

+runtest("LineParse.bpl")

+runtest("LineResolve.bpl")

+runtest("AttributeParsingErr.bpl")

+#runtest("/print:- /env:0 AttributeParsing.bpl")

+runtest("AttributeResolution.bpl")

+#runtest("/print:- /env:0 Quoting.bpl")

+runtest("LargeLiterals0.bpl")

+runtest("MapsResolutionErrors.bpl")

+runtest("Orderings.bpl")

+runtest("BadQuantifier.bpl")

+#runtest("EmptyCallArgs.bpl")

+runtest("SeparateVerification0.bpl")

+runtest("SeparateVerification1.bpl SeparateVerification0.bpl")

+runtest("SeparateVerification0.bpl SeparateVerification0.bpl")

+#runtest("SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl")

+

+# compare the output with the expected answers

+test_file = open("Output").readlines()

+correct_file = open("Answer").readlines()

+

+for test, correct in zip(test_file, correct_file):

+    if test.strip(' \t\n\r') != correct.strip(' \t\n\r'):

+        print "\n===== " + os.getcwd().split(os.sep)[-1] + ": FAILED"

+        break

+else:

+    print "\n===== " + os.getcwd().split(os.sep)[-1] + ": PASSED"

diff --git a/Test/test1/runtest.py b/Test/test1/runtest.py
new file mode 100755
index 00000000..4ef5dd85
--- /dev/null
+++ b/Test/test1/runtest.py
@@ -0,0 +1,74 @@
+#!/usr/bin/python

+

+# 2013 Pantazis Deligiannis

+#

+# runs the test cases of this directory

+

+import sys;

+import os;

+import getopt;

+

+MONO = "/usr/bin/mono "

+BOOGIE = "/Users/pantazis/workspace/boogie/Binaries/Boogie.exe "

+

+PROVER_OPTIONS_Z3 = "/nologo "

+PROVER_OPTIONS_CVC4 = "/proverOpt:SOLVER=cvc4 /nologo "

+

+# choose a parser

+opts, args = getopt.getopt(sys.argv[1:], "s:", ["solver="])

+solver = "Z3"

+for o, a in opts:

+  if o in ("-s", "--solver"):

+      if a == "cvc4":

+          solver = a

+

+# if the Output file exists remove it

+if os.path.exists("Output"):

+  os.remove("Output")

+

+# runs the given test

+def runtest(filename):

+  if solver == "cvc4":

+    if os.name == "nt":

+      command = BOOGIE + PROVER_OPTIONS_CVC4 + filename

+    else:

+	  command = MONO + BOOGIE + PROVER_OPTIONS_CVC4 + filename

+  else:

+    if os.name == "nt":

+      command = BOOGIE + PROVER_OPTIONS_Z3 + filename

+    else:

+	  command = MONO + BOOGIE + PROVER_OPTIONS_Z3 + filename

+  

+  print "===== Testing: " + filename

+  

+  if os.path.exists("Output"):

+    os.system(command + " >> Output")

+  else:

+    os.system(command + " > Output")

+    

+runtest("Frame0.bpl")

+runtest("Frame1.bpl")

+runtest("LogicalExprs.bpl")

+runtest("Arrays.bpl")

+runtest("WhereTyping.bpl")

+runtest("Family.bpl")

+runtest("AttributeTyping.bpl")

+runtest("UpdateExprTyping.bpl")

+runtest("MapsTypeErrors.bpl")

+runtest("Orderings.bpl")

+runtest("EmptyCallArgs.bpl")

+runtest("FunBody.bpl")

+runtest("IfThenElse0.bpl")

+runtest("Lambda.bpl")

+runtest("IntReal.bpl")

+

+# compare the output with the expected answers

+test_file = open("Output").readlines()

+correct_file = open("Answer").readlines()

+

+for test, correct in zip(test_file, correct_file):

+    if test.strip(' \t\n\r') != correct.strip(' \t\n\r'):

+        print "\n===== " + os.getcwd().split(os.sep)[-1] + ": FAILED"

+        break

+else:

+    print "\n===== " + os.getcwd().split(os.sep)[-1] + ": PASSED"

diff --git a/Test/test13/runtest.py b/Test/test13/runtest.py
new file mode 100755
index 00000000..f91fa9f9
--- /dev/null
+++ b/Test/test13/runtest.py
@@ -0,0 +1,62 @@
+#!/usr/bin/python

+

+# 2013 Pantazis Deligiannis

+#

+# runs the test cases of this directory

+

+import sys;

+import os;

+import getopt;

+

+MONO = "/usr/bin/mono "

+BOOGIE = "/Users/pantazis/workspace/boogie/Binaries/Boogie.exe "

+

+PROVER_OPTIONS_Z3 = "/nologo "

+PROVER_OPTIONS_CVC4 = "/proverOpt:SOLVER=cvc4 /nologo "

+

+# choose a parser

+opts, args = getopt.getopt(sys.argv[1:], "s:", ["solver="])

+solver = "Z3"

+for o, a in opts:

+  if o in ("-s", "--solver"):

+      if a == "cvc4":

+          solver = a

+

+# if the Output file exists remove it

+if os.path.exists("Output"):

+  os.remove("Output")

+

+# runs the given test

+def runtest(filename):

+  if solver == "cvc4":

+    if os.name == "nt":

+      command = BOOGIE + PROVER_OPTIONS_CVC4 + filename

+    else:

+	  command = MONO + BOOGIE + PROVER_OPTIONS_CVC4 + filename

+  else:

+    if os.name == "nt":

+      command = BOOGIE + PROVER_OPTIONS_Z3 + filename

+    else:

+	  command = MONO + BOOGIE + PROVER_OPTIONS_Z3 + filename

+  

+  print "===== Testing: " + filename

+  

+  if os.path.exists("Output"):

+    os.system(command + " >> Output")

+  else:

+    os.system(command + " > Output")

+

+os.system("echo >> Output")

+os.system("echo -------------------- ErrorTraceTestLoopInvViolationBPL -------------------- >> Output")

+runtest("ErrorTraceTestLoopInvViolationBPL.bpl")

+

+# compare the output with the expected answers

+test_file = open("Output").readlines()

+correct_file = open("Answer").readlines()

+

+for test, correct in zip(test_file, correct_file):

+    if test.strip(' \t\n\r') != correct.strip(' \t\n\r'):

+        print "\n===== " + os.getcwd().split(os.sep)[-1] + ": FAILED"

+        break

+else:

+    print "\n===== " + os.getcwd().split(os.sep)[-1] + ": PASSED"

diff --git a/Test/test15/runtest.py b/Test/test15/runtest.py
new file mode 100755
index 00000000..ec2b40ca
--- /dev/null
+++ b/Test/test15/runtest.py
@@ -0,0 +1,73 @@
+#!/usr/bin/python

+

+# 2013 Pantazis Deligiannis

+#

+# runs the test cases of this directory

+

+import sys;

+import os;

+import getopt;

+

+MONO = "/usr/bin/mono "

+BOOGIE = "/Users/pantazis/workspace/boogie/Binaries/Boogie.exe "

+

+PROVER_OPTIONS_Z3 = "/nologo "

+PROVER_OPTIONS_CVC4 = "/proverOpt:SOLVER=cvc4 /nologo "

+

+# choose a parser

+opts, args = getopt.getopt(sys.argv[1:], "s:", ["solver="])

+solver = "Z3"

+for o, a in opts:

+  if o in ("-s", "--solver"):

+      if a == "cvc4":

+          solver = a

+

+# if the Output file exists remove it

+if os.path.exists("Output"):

+  os.remove("Output")

+

+# runs the given test

+def runtest(filename):

+  if solver == "cvc4":

+    if os.name == "nt":

+      command = BOOGIE + PROVER_OPTIONS_CVC4 + filename

+    else:

+	  command = MONO + BOOGIE + PROVER_OPTIONS_CVC4 + filename

+  else:

+    if os.name == "nt":

+      command = BOOGIE + PROVER_OPTIONS_Z3 + filename

+    else:

+	  command = MONO + BOOGIE + PROVER_OPTIONS_Z3 + filename

+  

+  print "===== Testing: " + filename

+  

+  if os.path.exists("Output"):

+    os.system(command + " >> Output")

+  else:

+    os.system(command + " > Output")

+    

+files = ["NullInModel", "IntInModel", "ModelTest"]

+

+for file in files:

+  os.system("echo >> Output")

+  os.system("echo -------------------- " + file + " -------------------- >> Output")

+  runtest(file + ".bpl /printModel:2")

+  

+os.system("echo >> Output")

+os.system("echo -------------------- InterpretedFunctionTests -------------------- >> Output")

+runtest("InterpretedFunctionTests.bpl")

+

+os.system("echo >> Output")

+os.system("echo -------------------- CaptureState -------------------- >> Output")

+runtest("CaptureState.bpl /mv:-")

+

+# compare the output with the expected answers

+test_file = open("Output").readlines()

+correct_file = open("Answer").readlines()

+

+for test, correct in zip(test_file, correct_file):

+    if test.strip(' \t\n\r') != correct.strip(' \t\n\r'):

+        print "\n===== " + os.getcwd().split(os.sep)[-1] + ": FAILED"

+        break

+else:

+    print "\n===== " + os.getcwd().split(os.sep)[-1] + ": PASSED"

diff --git a/Test/test16/runtest.py b/Test/test16/runtest.py
new file mode 100755
index 00000000..2106e291
--- /dev/null
+++ b/Test/test16/runtest.py
@@ -0,0 +1,67 @@
+#!/usr/bin/python

+

+# 2013 Pantazis Deligiannis

+#

+# runs the test cases of this directory

+

+import sys;

+import os;

+import getopt;

+

+MONO = "/usr/bin/mono "

+BOOGIE = "/Users/pantazis/workspace/boogie/Binaries/Boogie.exe "

+

+PROVER_OPTIONS_Z3 = "/nologo "

+PROVER_OPTIONS_CVC4 = "/proverOpt:SOLVER=cvc4 /nologo "

+

+# choose a parser

+opts, args = getopt.getopt(sys.argv[1:], "s:", ["solver="])

+solver = "Z3"

+for o, a in opts:

+  if o in ("-s", "--solver"):

+      if a == "cvc4":

+          solver = a

+

+# if the Output file exists remove it

+if os.path.exists("Output"):

+  os.remove("Output")

+

+# runs the given test

+def runtest(filename):

+  if solver == "cvc4":

+    if os.name == "nt":

+      command = BOOGIE + PROVER_OPTIONS_CVC4 + filename

+    else:

+	  command = MONO + BOOGIE + PROVER_OPTIONS_CVC4 + filename

+  else:

+    if os.name == "nt":

+      command = BOOGIE + PROVER_OPTIONS_Z3 + filename

+    else:

+	  command = MONO + BOOGIE + PROVER_OPTIONS_Z3 + filename

+  

+  print "===== Testing: " + filename

+  

+  if os.path.exists("Output"):

+    os.system(command + " >> Output")

+  else:

+    os.system(command + " > Output")

+    

+os.system("echo -------------------- LoopUnroll.bpl /loopUnroll:1 -------------------- >> Output")

+runtest("/loopUnroll:1 /logPrefix:-lu1 LoopUnroll.bpl")

+

+os.system("echo -------------------- LoopUnroll.bpl /loopUnroll:2 -------------------- >> Output")

+runtest("LoopUnroll.bpl /logPrefix:-lu2 /proc:ManyIterations /loopUnroll:2")

+

+os.system("echo -------------------- LoopUnroll.bpl /loopUnroll:3 -------------------- >> Output")

+runtest("LoopUnroll.bpl /logPrefix:-lu3 /proc:ManyIterations /loopUnroll:3")

+

+# compare the output with the expected answers

+test_file = open("Output").readlines()

+correct_file = open("Answer").readlines()

+

+for test, correct in zip(test_file, correct_file):

+    if test.strip(' \t\n\r') != correct.strip(' \t\n\r'):

+        print "\n===== " + os.getcwd().split(os.sep)[-1] + ": FAILED"

+        break

+else:

+    print "\n===== " + os.getcwd().split(os.sep)[-1] + ": PASSED"

diff --git a/Test/test17/runtest.py b/Test/test17/runtest.py
new file mode 100755
index 00000000..86681f2a
--- /dev/null
+++ b/Test/test17/runtest.py
@@ -0,0 +1,65 @@
+#!/usr/bin/python

+

+# 2013 Pantazis Deligiannis

+#

+# runs the test cases of this directory

+

+import sys;

+import os;

+import getopt;

+

+MONO = "/usr/bin/mono "

+BOOGIE = "/Users/pantazis/workspace/boogie/Binaries/Boogie.exe "

+

+PROVER_OPTIONS_Z3 = "/nologo "

+PROVER_OPTIONS_CVC4 = "/proverOpt:SOLVER=cvc4 /nologo "

+

+# choose a parser

+opts, args = getopt.getopt(sys.argv[1:], "s:", ["solver="])

+solver = "Z3"

+for o, a in opts:

+  if o in ("-s", "--solver"):

+      if a == "cvc4":

+          solver = a

+

+# if the Output file exists remove it

+if os.path.exists("Output"):

+  os.remove("Output")

+

+# runs the given test

+def runtest(filename):

+  if solver == "cvc4":

+    if os.name == "nt":

+      command = BOOGIE + PROVER_OPTIONS_CVC4 + filename

+    else:

+	  command = MONO + BOOGIE + PROVER_OPTIONS_CVC4 + filename

+  else:

+    if os.name == "nt":

+      command = BOOGIE + PROVER_OPTIONS_Z3 + filename

+    else:

+	  command = MONO + BOOGIE + PROVER_OPTIONS_Z3 + filename

+  

+  print "===== Testing: " + filename

+  

+  if os.path.exists("Output"):

+    os.system(command + " >> Output")

+  else:

+    os.system(command + " > Output")

+    

+files = ["contractinfer", "flpydisk"]

+

+for file in files:

+  os.system("echo >> Output")

+  os.system("echo -------------------- " + file + " -------------------- >> Output")

+  runtest("/errorLimit:1 /contractInfer /z3mam:4 /subsumption:0 " + file + ".bpl")

+

+# compare the output with the expected answers

+test_file = open("Output").readlines()

+correct_file = open("Answer").readlines()

+

+for test, correct in zip(test_file, correct_file):

+    if test.strip(' \t\n\r') != correct.strip(' \t\n\r'):

+        print "\n===== " + os.getcwd().split(os.sep)[-1] + ": FAILED"

+        break

+else:

+    print "\n===== " + os.getcwd().split(os.sep)[-1] + ": PASSED"

diff --git a/Test/test2/runtest.py b/Test/test2/runtest.py
new file mode 100755
index 00000000..978343da
--- /dev/null
+++ b/Test/test2/runtest.py
@@ -0,0 +1,92 @@
+#!/usr/bin/python

+

+# 2013 Pantazis Deligiannis

+#

+# runs the test cases of this directory

+

+import sys;

+import os;

+import getopt;

+

+MONO = "/usr/bin/mono "

+BOOGIE = "/Users/pantazis/workspace/boogie/Binaries/Boogie.exe "

+

+PROVER_OPTIONS_Z3 = "/nologo "

+PROVER_OPTIONS_CVC4 = "/proverOpt:SOLVER=cvc4 /nologo "

+

+# choose a parser

+opts, args = getopt.getopt(sys.argv[1:], "s:", ["solver="])

+solver = "Z3"

+for o, a in opts:

+  if o in ("-s", "--solver"):

+      if a == "cvc4":

+          solver = a

+

+# if the Output file exists remove it

+if os.path.exists("Output"):

+  os.remove("Output")

+

+# runs the given test

+def runtest(filename):

+  if solver == "cvc4":

+    if os.name == "nt":

+      command = BOOGIE + PROVER_OPTIONS_CVC4 + filename

+    else:

+	  command = MONO + BOOGIE + PROVER_OPTIONS_CVC4 + filename

+  else:

+    if os.name == "nt":

+      command = BOOGIE + PROVER_OPTIONS_Z3 + filename

+    else:

+	  command = MONO + BOOGIE + PROVER_OPTIONS_Z3 + filename

+  

+  print "===== Testing: " + filename

+  

+  if os.path.exists("Output"):

+    os.system(command + " >> Output")

+  else:

+    os.system(command + " > Output")

+

+files = ["FormulaTerm.bpl", "FormulaTerm2.bpl", "Passification.bpl", "B.bpl",

+  "Ensures.bpl", "Old.bpl", "OldIllegal.bpl", "Arrays.bpl", "Axioms.bpl",

+  "Quantifiers.bpl", "Call.bpl", "AssumeEnsures.bpl",

+  "CutBackEdge.bpl", "False.bpl", "LoopInvAssume.bpl",

+  "strings-no-where.bpl", "strings-where.bpl",

+  "Structured.bpl", "Where.bpl", "UpdateExpr.bpl",

+  "NeverPattern.bpl", "NullaryMaps.bpl", "Implies.bpl",

+  "IfThenElse1.bpl", "Lambda.bpl", "LambdaPoly.bpl", "LambdaOldExpressions.bpl",

+  "SelectiveChecking.bpl", "FreeCall.bpl"]

+

+for file in files:

+  os.system("echo >> Output")

+  os.system("echo -------------------- " + file + " -------------------- >> Output")

+  runtest("/noinfer " + file)

+  

+files = ["Arrays.bpl", "Lambda.bpl", "TypeEncodingM.bpl"]

+

+for file in files:

+  os.system("echo >> Output")

+  os.system("echo -------------------- " + file + " /typeEncoding:m -------------------- >> Output")

+  runtest("/noinfer /typeEncoding:m " + file)

+  

+os.system("echo >> Output")

+os.system("echo -------------------- sk_hack.bpl -------------------- >> Output")

+runtest("/noinfer sk_hack.bpl")

+

+os.system("echo >> Output")

+os.system("echo -------------------- ContractEvaluationOrder.bpl -------------------- >> Output")

+runtest("ContractEvaluationOrder.bpl")

+

+os.system("echo >> Output")

+os.system("echo -------------------- Timeouts0.bpl -------------------- >> Output")

+runtest("/timeLimit:4 Timeouts0.bpl")

+

+# compare the output with the expected answers

+test_file = open("Output").readlines()

+correct_file = open("Answer").readlines()

+

+for test, correct in zip(test_file, correct_file):

+    if test.strip(' \t\n\r') != correct.strip(' \t\n\r'):

+        print "\n===== " + os.getcwd().split(os.sep)[-1] + ": FAILED"

+        break

+else:

+    print "\n===== " + os.getcwd().split(os.sep)[-1] + ": PASSED"

diff --git a/Test/test20/runtest.py b/Test/test20/runtest.py
new file mode 100755
index 00000000..8617c858
--- /dev/null
+++ b/Test/test20/runtest.py
@@ -0,0 +1,79 @@
+#!/usr/bin/python

+

+# 2013 Pantazis Deligiannis

+#

+# runs the test cases of this directory

+

+import sys;

+import os;

+import getopt;

+

+MONO = "/usr/bin/mono "

+BOOGIE = "/Users/pantazis/workspace/boogie/Binaries/Boogie.exe "

+

+PROVER_OPTIONS_Z3 = "/nologo "

+PROVER_OPTIONS_CVC4 = "/proverOpt:SOLVER=cvc4 /nologo "

+

+# choose a parser

+opts, args = getopt.getopt(sys.argv[1:], "s:", ["solver="])

+solver = "Z3"

+for o, a in opts:

+  if o in ("-s", "--solver"):

+      if a == "cvc4":

+          solver = a

+

+# if the Output file exists remove it

+if os.path.exists("Output"):

+  os.remove("Output")

+

+# runs the given test

+def runtest(filename):

+  if solver == "cvc4":

+    if os.name == "nt":

+      command = BOOGIE + PROVER_OPTIONS_CVC4 + filename

+    else:

+	  command = MONO + BOOGIE + PROVER_OPTIONS_CVC4 + filename

+  else:

+    if os.name == "nt":

+      command = BOOGIE + PROVER_OPTIONS_Z3 + filename

+    else:

+	  command = MONO + BOOGIE + PROVER_OPTIONS_Z3 + filename

+  

+  print "===== Testing: " + filename

+  

+  if os.path.exists("Output"):

+    os.system(command + " >> Output")

+  else:

+    os.system(command + " > Output")

+    

+runtest("TypeDecls0.bpl")

+runtest("TypeDecls1.bpl")

+runtest("Prog0.bpl")

+runtest("Prog1.bpl")

+runtest("Prog2.bpl")

+runtest("PolyFuns0.bpl")

+runtest("PolyFuns1.bpl")

+runtest("PolyProcs0.bpl")

+runtest("TypeSynonyms0.bpl")

+runtest("TypeSynonyms1.bpl")

+runtest("TypeSynonyms2.bpl")

+runtest("/print:- /env:0 TypeSynonyms0.bpl")

+runtest("/print:- /env:0 /printDesugared TypeSynonyms2.bpl")

+runtest("PolyPolyPoly.bpl")

+runtest("PolyPolyPoly2.bpl")

+runtest("ProcParamReordering.bpl")

+runtest("ParallelAssignment.bpl")

+runtest("ParallelAssignment2.bpl")

+runtest("Coercions.bpl")

+runtest("EmptySeq.bpl")

+

+# compare the output with the expected answers

+test_file = open("Output").readlines()

+correct_file = open("Answer").readlines()

+

+for test, correct in zip(test_file, correct_file):

+    if test.strip(' \t\n\r') != correct.strip(' \t\n\r'):

+        print "\n===== " + os.getcwd().split(os.sep)[-1] + ": FAILED"

+        break

+else:

+    print "\n===== " + os.getcwd().split(os.sep)[-1] + ": PASSED"

diff --git a/Test/test21/runtest.py b/Test/test21/runtest.py
new file mode 100755
index 00000000..f42d7665
--- /dev/null
+++ b/Test/test21/runtest.py
@@ -0,0 +1,90 @@
+#!/usr/bin/python

+

+# 2013 Pantazis Deligiannis

+#

+# runs the test cases of this directory

+

+import sys;

+import os;

+import getopt;

+

+MONO = "/usr/bin/mono "

+BOOGIE = "/Users/pantazis/workspace/boogie/Binaries/Boogie.exe "

+

+PROVER_OPTIONS_Z3 = "/nologo "

+PROVER_OPTIONS_CVC4 = "/proverOpt:SOLVER=cvc4 /nologo "

+

+# choose a parser

+opts, args = getopt.getopt(sys.argv[1:], "s:", ["solver="])

+solver = "Z3"

+for o, a in opts:

+  if o in ("-s", "--solver"):

+      if a == "cvc4":

+          solver = a

+

+# if the Output file exists remove it

+if os.path.exists("Output"):

+  os.remove("Output")

+

+# runs the given test

+def runtest(filename):

+  if solver == "cvc4":

+    if os.name == "nt":

+      command = BOOGIE + PROVER_OPTIONS_CVC4 + filename

+    else:

+	  command = MONO + BOOGIE + PROVER_OPTIONS_CVC4 + filename

+  else:

+    if os.name == "nt":

+      command = BOOGIE + PROVER_OPTIONS_Z3 + filename

+    else:

+	  command = MONO + BOOGIE + PROVER_OPTIONS_Z3 + filename

+  

+  print "===== Testing: " + filename

+  

+  if os.path.exists("Output"):

+    os.system(command + " >> Output")

+  else:

+    os.system(command + " > Output")

+    

+modes = ["n", "p", "a"]

+

+files = ["DisjointDomains.bpl", "DisjointDomains2.bpl", "FunAxioms.bpl",

+  "FunAxioms2.bpl", "PolyList.bpl", "Maps0.bpl", "Maps1.bpl",

+  "InterestingExamples0.bpl", "InterestingExamples1.bpl", "InterestingExamples2.bpl",

+  "InterestingExamples3.bpl", "InterestingExamples4.bpl", "InterestingExamples5.bpl",

+  "Colors.bpl", "HeapAbstraction.bpl", "HeapAxiom.bpl", "Triggers0.bpl", "Triggers1.bpl",

+  "Keywords.bpl", "Casts.bpl", "BooleanQuantification.bpl", "EmptyList.bpl", "Boxing.bpl",

+  "MapOutputTypeParams.bpl", "ParallelAssignment.bpl", "BooleanQuantification2.bpl",

+  "Flattening.bpl", "Orderings.bpl", "Orderings2.bpl", "Orderings3.bpl", "Orderings4.bpl",

+  "EmptySetBug.bpl", "Coercions2.bpl", "MapAxiomsConsistency.bpl", "LargeLiterals0.bpl",

+  "Real.bpl"]

+

+for mode in modes:

+  os.system("echo >> Output")

+  os.system("echo --------------------- TypeEncoding " + mode + " z3types ---------------------------- >> Output")

+  for file in files:

+    os.system("echo --------------------- File " + file + " ---------------------------- >> Output")

+    runtest("/typeEncoding:" + mode + " /logPrefix:0" + mode + " " + file)

+

+  os.system("echo --------------------- File NameClash.bpl ---------------------------- >> Output")

+  runtest("/typeEncoding:" + mode + " /logPrefix:0" + mode + " NameClash.bpl")

+

+  os.system("echo --------------------- File Keywords.bpl ---------------------------- >> Output")

+  runtest("/typeEncoding:" + mode + " /logPrefix:0" + mode + " Keywords.bpl")

+

+  os.system("echo --------------------- File LargeLiterals0.bpl ---------------------------- >> Output")

+  runtest("/typeEncoding:" + mode + " /logPrefix:0" + mode + " LargeLiterals0.bpl")

+

+  os.system("echo --------------------- File LetSorting.bpl ---------------------------- >> Output")

+  runtest("/typeEncoding:" + mode + " /logPrefix:0" + mode + " LetSorting.bpl")

+

+# compare the output with the expected answers

+test_file = open("Output").readlines()

+correct_file = open("Answer").readlines()

+

+for test, correct in zip(test_file, correct_file):

+    if test.strip(' \t\n\r') != correct.strip(' \t\n\r'):

+        print "\n===== " + os.getcwd().split(os.sep)[-1] + ": FAILED"

+        break

+else:

+    print "\n===== " + os.getcwd().split(os.sep)[-1] + ": PASSED"

diff --git a/Test/test7/runtest.py b/Test/test7/runtest.py
new file mode 100755
index 00000000..9b0e557f
--- /dev/null
+++ b/Test/test7/runtest.py
@@ -0,0 +1,89 @@
+#!/usr/bin/python

+

+# 2013 Pantazis Deligiannis

+#

+# runs the test cases of this directory

+

+import sys;

+import os;

+import getopt;

+

+MONO = "/usr/bin/mono "

+BOOGIE = "/Users/pantazis/workspace/boogie/Binaries/Boogie.exe "

+

+PROVER_OPTIONS_Z3 = "/nologo "

+PROVER_OPTIONS_CVC4 = "/proverOpt:SOLVER=cvc4 /nologo "

+

+# choose a parser

+opts, args = getopt.getopt(sys.argv[1:], "s:", ["solver="])

+solver = "Z3"

+for o, a in opts:

+  if o in ("-s", "--solver"):

+      if a == "cvc4":

+          solver = a

+

+# if the Output file exists remove it

+if os.path.exists("Output"):

+  os.remove("Output")

+

+# runs the given test

+def runtest(filename):

+  if solver == "cvc4":

+    if os.name == "nt":

+      command = BOOGIE + PROVER_OPTIONS_CVC4 + filename

+    else:

+	  command = MONO + BOOGIE + PROVER_OPTIONS_CVC4 + filename

+  else:

+    if os.name == "nt":

+      command = BOOGIE + PROVER_OPTIONS_Z3 + filename

+    else:

+	  command = MONO + BOOGIE + PROVER_OPTIONS_Z3 + filename

+  

+  print "===== Testing: " + filename

+  

+  if filename == "SeparateVerification0.bpl":

+    os.system("echo ----- SeparateVerification0.bpl >> Output")

+  elif filename == "SeparateVerification1.bpl SeparateVerification0.bpl":

+    os.system("echo ----- SeparateVerification1.bpl SeparateVerification0.bpl >> Output")

+  elif filename == "SeparateVerification0.bpl SeparateVerification0.bpl":

+    os.system("echo ----- SeparateVerification0.bpl SeparateVerification0.bpl >> Output")

+  elif filename == "SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl":

+    os.system("echo ----- SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl >> Output")

+  

+  if os.path.exists("Output"):

+    os.system(command + " >> Output")

+  else:

+    os.system(command + " > Output")

+

+os.system("echo ------------------------------ NestedVC.bpl --------------------- >> Output")

+runtest("/vc:nested NestedVC.bpl")

+

+os.system("echo ------------------------------ UnreachableBlocks.bpl --------------------- >> Output")

+runtest("/vc:nested UnreachableBlocks.bpl")

+

+os.system("echo ------------------------------ MultipleErrors.bpl --------------------- >> Output")

+

+modes = ["block", "local", "dag"]

+

+for mode in modes:

+  os.system("echo >> Output")

+  os.system("echo ----- /vc:" + mode + " >> Output")

+  runtest("/errorLimit:1 /errorTrace:1 /vc:" + mode + " /logPrefix:-1" + mode + " MultipleErrors.bpl")

+

+modes = ["local", "dag"]

+

+for mode in modes:

+  os.system("echo >> Output")

+  os.system("echo ----- /errorLimit:10 /vc:" + mode + " >> Output")

+  runtest("/errorLimit:10 /errorTrace:1 /vc:" + mode + " /logPrefix:-10" + mode + " MultipleErrors.bpl")

+

+# compare the output with the expected answers

+test_file = open("Output").readlines()

+correct_file = open("Answer").readlines()

+

+for test, correct in zip(test_file, correct_file):

+    if test.strip(' \t\n\r') != correct.strip(' \t\n\r'):

+        print "\n===== " + os.getcwd().split(os.sep)[-1] + ": FAILED"

+        break

+else:

+    print "\n===== " + os.getcwd().split(os.sep)[-1] + ": PASSED"