diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-08 17:56:46 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-08 17:56:46 -0500 |
| commit | c2393be5f0385609a1fe7cfe76f5665ec53cf4a1 (patch) | |
| tree | 816676ad664f9f97e613923a871d007d498a4fd8 /test/regress | |
| parent | 7ce4d047670810a10a3f0fc202cd7d94bb4b7e69 (diff) | |
SMT-LIB get-model output now is easier to machine-parse: contains (model...) bracketing
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress0/bug411.smt2 | 2 |
1 files changed, 2 insertions, 0 deletions
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) |