Merge pull request #485 from ethereum/smt_fix_z3

Don't check SMTChecker test if timeout

test/smtcallback.js

@@ -158,6 +158,15 @@ tape('SMTCheckerCallback', function (t) {
     // Run all tests
     for (i in tests) {
       var test = tests[i];
+
+      // Z3's nondeterminism sometimes causes a test to timeout in one context but not in the other,
+      // so if we see timeout we skip a potentially misleading run.
+      var findError = (errorMsg) => { return errorMsg.includes('Error trying to invoke SMT solver'); };
+      if (test.expectations.find(findError) !== undefined) {
+        st.skip('Test contains timeout which may have been caused by nondeterminism.');
+        continue;
+      }
+
       var output = JSON.parse(solc.compile(
         JSON.stringify({
           language: 'Solidity',
@@ -180,6 +189,11 @@ tape('SMTCheckerCallback', function (t) {
         continue;
       }
 
+      if (test.errors.find(findError) !== undefined) {
+        st.skip('Test contains timeout which may have been caused by nondeterminism.');
+        continue;
+      }
+
       // Compare expected vs obtained errors
       st.ok(expectErrors(test.expectations, test.errors));
     }