Fix model parsing for Boolector 3.2.2 (emina#206)

The latest Boolector release [changed][] the format of SMT models to conform to the SMT-LIB spec by not including the `model` symbol, which our parser was expecting (mostly because that's what Z3 does). It's not hard to support both versions, so let's do that. [changed]: Boolector/boolector@5c862bc
jamestiotio · Nov 11, 2021 · 2e2896d · 2e2896d
1 parent dbfd847
commit 2e2896d
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/rosette/solver/smt/boolector.rkt b/rosette/solver/smt/boolector.rkt
@@ -122,9 +122,8 @@
          [(== 'sat)
           (server-write server (get-model))
           (match (server-read server (read))
-            [(list (== 'model) def ...)
-             (for/hash ([d def] #:when (and (pair? d) (equal? (car d) 'define-fun)))
-               (values (cadr d) d))]
+            [(list (== 'model) ... (and def (list (== 'define-fun) _ ...)) ...)
+             (for/hash ([d def]) (values (cadr d) d))]
             [other (error 'read-solution "expected model, given ~a" other)])]
          [(== 'unsat) 'unsat]
          [(== 'unknown) 'unknown]