Prevent division by zero in Z3

1 files changed, 8 insertions, 2 deletions

diff --git a/Assignment2/src/Z3.icl b/Assignment2/src/Z3.icl
index ca869a1..4db349e 100644
--- a/Assignment2/src/Z3.icl
+++ b/Assignment2/src/Z3.icl
@@ -1,5 +1,7 @@
 implementation module Z3
 
+import StdList
+import StdMisc
 import StdString
 
 import System.Process
@@ -43,13 +45,17 @@ addVariable z3 type s w
 # (_, w) = writePipe (trace_id $ "(declare-const " <+ s <+ " " <+ type <+ ")\n") z3.Z3.stdIn w
 = w
 
-checkSat :: !Z3 !*World -> (!Bool, !*World)
+checkSat :: !Z3 !*World -> (!Satisfaction, !*World)
 checkSat z3 w
 # (_, w) = writePipe "(check-sat)\n" z3.Z3.stdIn w
 # (out, w) = readPipeBlocking z3.Z3.stdOut w
 # out = fromOk out
 # out = trace_id out
-= (endsWith "sat\n" out, w)
+= (case last $ init $ split "\n" out of
+	"sat"     -> Sat
+	"unsat"   -> Unsat
+	"unknown" -> Unknown
+	_         -> abort "Z3 failed\n", w)
 
 getModel :: !Z3 !*World -> (!String, !*World)
 getModel z3 w