From 37e1a756c83a24322f1cb496dbd2e85a162c93b0 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sat, 21 Jun 2014 22:09:17 -0400
Subject: [PATCH] Run in application track with --check-models.

---
 contrib/run-script-smtcomp2014-application | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/contrib/run-script-smtcomp2014-application b/contrib/run-script-smtcomp2014-application
index fb4ebe259..165293e74 100755
--- a/contrib/run-script-smtcomp2014-application
+++ b/contrib/run-script-smtcomp2014-application
@@ -19,7 +19,7 @@ function runcvc4 {
   # we run in this way for line-buffered input, otherwise memory's a
   # concern (plus it mimics what we'll end up getting from an
   # application-track trace runner?)
-  (echo "(set-logic $logic)"; cat) | $cvc4 -L smt2 --print-success --no-checking --no-interactive --tear-down-incremental "$@"
+  (echo "(set-logic $logic)"; cat) | $cvc4 -L smt2 --print-success --no-checking --no-interactive --tear-down-incremental --check-models "$@"
 }
 
 case "$logic" in
-- 
2.30.2