From 0b63afd6442b9d41e21227a130755e329d554cbe Mon Sep 17 00:00:00 2001 From: William Wang Date: Fri, 13 Dec 2024 12:23:57 +0000 Subject: [PATCH] Adapt z3 constraint checking logic to windows On Windows, the output of z3 has a trailing \r, which makes checking of result = 'unsat' return false. Checking the prefix of the output is enough and it adapts to different types of OS. --- src/lib/constraint.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/lib/constraint.ml b/src/lib/constraint.ml index a5b9256b5..4098a200d 100644 --- a/src/lib/constraint.ml +++ b/src/lib/constraint.ml @@ -407,11 +407,11 @@ let rec call_smt' l abstract extra constraints = in Sys.remove input_file; try - let _problem, _ = List.find (fun (_, result) -> result = "unsat") smt_output in + let _problem, _ = List.find (fun (_, result) -> String.starts_with ~prefix:"unsat" result) smt_output in known_problems := DigestMap.add digest Unsat !known_problems; Unsat with Not_found -> - let unsolved = List.filter (fun (_, result) -> result = "unknown") smt_output in + let unsolved = List.filter (fun (_, result) -> String.starts_with ~prefix:"unknown" result) smt_output in if unsolved == [] then ( known_problems := DigestMap.add digest Sat !known_problems; Sat