From c2393be5f0385609a1fe7cfe76f5665ec53cf4a1 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 8 Jan 2013 17:56:46 -0500
Subject: SMT-LIB get-model output now is easier to machine-parse: contains
 (model...) bracketing

---
 test/regress/regress0/bug411.smt2 | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'test/regress/regress0')

diff --git a/test/regress/regress0/bug411.smt2 b/test/regress/regress0/bug411.smt2
index af9acb97a..3e33c9cd5 100644
--- a/test/regress/regress0/bug411.smt2
+++ b/test/regress/regress0/bug411.smt2
@@ -1,5 +1,7 @@
 ; EXPECT: sat
+; EXPECT: (model
 ; EXPECT: (define-fun x () Int 5)
+; EXPECT: )
 ; EXIT: 10
 (set-option :produce-models true)
 (set-logic QF_UFLIA)
-- 
cgit v1.2.3