Added a sanity check to lit configuration so tests won't run

if solver executables are missing.

1 files changed, 17 insertions, 4 deletions

diff --git a/Test/lit.site.cfg b/Test/lit.site.cfg
index ba162703..f9bed3c8 100644
--- a/Test/lit.site.cfg
+++ b/Test/lit.site.cfg
@@ -65,10 +65,9 @@ repositoryRoot = up(
                    )
 lit_config.note('Repository root is {}'.format(repositoryRoot))
 
-boogieExecutable = os.path.join( repositoryRoot,
-                                     'Binaries',
-                                     'Boogie.exe'
-                                   )
+binaryDir = os.path.join( repositoryRoot, 'Binaries')
+boogieExecutable = os.path.join( binaryDir, 'Boogie.exe')
+
 if not os.path.exists(boogieExecutable):
     lit_config.fatal('Could not find Boogie.exe at {}'.format(boogieExecutable))
 
@@ -91,6 +90,20 @@ lit_config.note('Using Boogie: {}\n'.format(boogieExecutable))
 
 config.substitutions.append( ('%boogie', boogieExecutable) )
 
+# Sanity check: Check solver executable is available
+solvers = ['z3.exe','cvc4.exe']
+solverFound = False
+for solver in solvers:
+    if os.path.exists( os.path.join(binaryDir, solver)):
+        solverFound = True
+
+if not solverFound:
+    lit_config.fatal('Could not find solver in "{binaryDir}". Tried looking for {solvers}'.format(
+                       binaryDir=binaryDir,
+                       solvers=solvers
+                       )
+                    )
+
 # Add diff tool substitution
 diffExecutable = None
 if os.name == 'posix':