From 863dd51bd8b5d72d41006a02950de28fc1666f21 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 4 Dec 2013 16:04:14 -0500
Subject: Don't put define-funs in model output; bug 411 testcase no longer
 relevant.

---
 test/regress/regress0/Makefile.am | 1 -
 test/regress/regress0/bug411.smt2 | 9 ---------
 2 files changed, 10 deletions(-)
 delete mode 100644 test/regress/regress0/bug411.smt2

(limited to 'test')

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 1e3e7c112..1daa0d1e8 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -136,7 +136,6 @@ BUG_TESTS = \
 	bug382.smt2 \
 	bug383.smt2 \
 	bug398.smt2 \
-	bug411.smt2 \
 	bug421.smt2 \
 	bug421b.smt2 \
 	bug425.cvc \
diff --git a/test/regress/regress0/bug411.smt2 b/test/regress/regress0/bug411.smt2
deleted file mode 100644
index 46ac4b544..000000000
--- a/test/regress/regress0/bug411.smt2
+++ /dev/null
@@ -1,9 +0,0 @@
-; EXPECT: sat
-; EXPECT: (model
-; EXPECT: (define-fun x () Int 5)
-; EXPECT: )
-(set-option :produce-models true)
-(set-logic QF_UFLIA)
-(define-fun x () Int 5)
-(check-sat)
-(get-model)
-- 
cgit v1.2.3