From 0223571987d100b0c9d12e59f8f40ecfd8ecb441 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Fri, 25 Sep 2020 18:43:10 +0200
Subject: [PATCH] [SMTChecker] Do not report error when rlimit

---
 libsmtutil/Z3CHCInterface.cpp                              | 7 +++++--
 .../smtCheckerTests/functions/functions_external_2.sol     | 1 -
 test/libsolidity/smtCheckerTests/imports/import_base.sol   | 1 -
 test/libsolidity/smtCheckerTests/loops/for_1_fail.sol      | 1 -
 .../smtCheckerTests/loops/for_1_false_positive.sol         | 1 -
 .../loops/while_loop_array_assignment_memory_memory.sol    | 1 -
 .../loops/while_loop_array_assignment_memory_storage.sol   | 1 -
 .../loops/while_loop_array_assignment_storage_storage.sol  | 2 --
 .../operators/compound_bitwise_or_int_1.sol                | 1 -
 .../operators/compound_bitwise_or_uint_1.sol               | 1 -
 .../operators/compound_bitwise_or_uint_2.sol               | 1 -
 .../operators/compound_bitwise_or_uint_3.sol               | 1 -
 12 files changed, 5 insertions(+), 14 deletions(-)

diff --git a/libsmtutil/Z3CHCInterface.cpp b/libsmtutil/Z3CHCInterface.cpp
index 2e11c7d0a..35b3556d9 100644
--- a/libsmtutil/Z3CHCInterface.cpp
+++ b/libsmtutil/Z3CHCInterface.cpp
@@ -95,9 +95,12 @@ pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression
 		}
 		// TODO retrieve model / invariants
 	}
-	catch (z3::exception const&)
+	catch (z3::exception const& _err)
 	{
-		result = CheckResult::ERROR;
+		if (_err.msg() == string("max. resource limit exceeded"))
+			result = CheckResult::UNKNOWN;
+		else
+			result = CheckResult::ERROR;
 		cex = {};
 	}
 
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol
index 975df538b..bc4694192 100644
--- a/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol
+++ b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol
@@ -17,5 +17,4 @@ contract C
 	}
 }
 // ----
-// Warning 1218: (297-321): Error trying to invoke SMT solver.
 // Warning 4661: (297-321): Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/imports/import_base.sol b/test/libsolidity/smtCheckerTests/imports/import_base.sol
index a65f8b3f5..d00534822 100644
--- a/test/libsolidity/smtCheckerTests/imports/import_base.sol
+++ b/test/libsolidity/smtCheckerTests/imports/import_base.sol
@@ -18,7 +18,6 @@ contract Der is Base {
 	}
 }
 // ----
-// Warning 1218: (der:101-109): Error trying to invoke SMT solver.
 // Warning 6328: (der:113-126): Assertion violation happens here.
 // Warning 2661: (base:100-103): Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 2661: (der:101-109): Overflow (resulting value larger than 2**256 - 1) happens here.
diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol b/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol
index 5588c6117..414a7861f 100644
--- a/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol
+++ b/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol
@@ -14,6 +14,5 @@ contract C
 // ====
 // SMTSolvers: z3
 // ----
-// Warning 1218: (176-181): Error trying to invoke SMT solver.
 // Warning 6328: (189-203): Assertion violation happens here.
 // Warning 2661: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here.
diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol
index eb45e7e2c..aff1b6852 100644
--- a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol
+++ b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol
@@ -14,5 +14,4 @@ contract C
 	}
 }
 // ----
-// Warning 1218: (176-181): Error trying to invoke SMT solver.
 // Warning 2661: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here.
diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol
index c8d533761..91a099d74 100644
--- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol
+++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol
@@ -19,7 +19,6 @@ contract LoopFor2 {
 // ====
 // SMTSolvers: z3
 // ----
-// Warning 1218: (244-249): Error trying to invoke SMT solver.
 // Warning 6328: (281-301): Assertion violation happens here.
 // Warning 6328: (305-324): Assertion violation happens here.
 // Warning 6328: (328-347): Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol
index 736b18caa..8612fede1 100644
--- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol
+++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol
@@ -23,6 +23,5 @@ contract LoopFor2 {
 // ====
 // SMTSolvers: z3
 // ----
-// Warning 1218: (237-242): Error trying to invoke SMT solver.
 // Warning 6328: (362-382): Assertion violation happens here.
 // Warning 6328: (409-428): Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
index 5d2bb0f0d..a4a93d163 100644
--- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
+++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
@@ -21,8 +21,6 @@ contract LoopFor2 {
 	}
 }
 // ----
-// Warning 1218: (229-234): Error trying to invoke SMT solver.
-// Warning 1218: (296-316): Error trying to invoke SMT solver.
 // Warning 6328: (320-339): Assertion violation happens here.
 // Warning 6328: (343-362): Assertion violation happens here.
 // Warning 4661: (296-316): Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol
index aaeb0d10a..e25ae354d 100644
--- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol
+++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol
@@ -9,4 +9,3 @@ contract C {
     }
 }
 // ----
-// Warning 1218: (174-212): Error trying to invoke SMT solver.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol
index b332e5bb4..790d30a76 100644
--- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol
+++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol
@@ -9,4 +9,3 @@ contract C {
     }
 }
 // ----
-// Warning 1218: (166-183): Error trying to invoke SMT solver.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol
index de45cd2ac..45bd12946 100644
--- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol
+++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol
@@ -11,5 +11,4 @@ contract C {
     }
 }
 // ----
-// Warning 1218: (173-192): Error trying to invoke SMT solver.
 // Warning 7812: (173-192): Assertion violation might happen here.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol
index 71a6cbac7..d135bd0cd 100644
--- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol
+++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol
@@ -10,5 +10,4 @@ contract C {
     }
 }
 // ----
-// Warning 1218: (157-172): Error trying to invoke SMT solver.
 // Warning 7812: (157-172): Assertion violation might happen here.