Skip to content

Commit 2795d8d

Browse files
committed
better handling of timeout in Z3
1 parent a5240ca commit 2795d8d

File tree

1 file changed

+6
-0
lines changed

1 file changed

+6
-0
lines changed

smt/lip6.smtlib.SMT/src/org/smtlib/solvers/Solver_z3_4_3.java

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -212,6 +212,12 @@ protected IResponse parseResponse(String response) {
212212
try {
213213
if (response.startsWith("stderr")) response = response.replace("stderr", "\"stderr\"");
214214
else if (response.startsWith("stdout")) response = response.replace("stdout", "\"stdout\"");
215+
216+
// check if we have timeout within last 50 char of the response
217+
if (response.substring(Math.max(0, response.length()-50)).contains("timeout")) {
218+
return smtConfig.responseFactory.error("Timeout of Z3 solver reached");
219+
}
220+
215221
Pattern oldbv = Pattern.compile("bv([0-9]+)\\[([0-9]+)\\]");
216222
Matcher mm = oldbv.matcher(response);
217223
while (mm.find()) {

0 commit comments

Comments
 (0)