From 55acdeb493ee3f9b66ed38f7526670b6e66c46bd Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Mon, 8 Oct 2018 17:34:35 -0700
Subject: [PATCH] Cmake: Fix ctest call for example/translator. (#2600)

example/translator expects an input file to translate but none was provided in the ctest call.
This caused the ctest call to hang and wait for input on stdin in some configurations (in
particular in the nightlies).
---
 examples/CMakeLists.txt                       |  4 +++-
 .../sets-translate-example-input.smt2         |  2 --
 examples/translator-example-input.smt2        | 20 +++++++++++++++++++
 3 files changed, 23 insertions(+), 3 deletions(-)
 create mode 100644 examples/translator-example-input.smt2

diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index 33d341ac8..68eb06074 100644
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -68,7 +68,9 @@ endmacro()
 set(EXAMPLES_LINK_LIBS cvc4 cvc4parser)
 cvc4_add_example(simple_vc_cxx "" "${EXAMPLES_LINK_LIBS}" "")
 cvc4_add_example(simple_vc_quant_cxx "" "${EXAMPLES_LINK_LIBS}" "")
-cvc4_add_example(translator "" "${EXAMPLES_LINK_LIBS}" "")
+cvc4_add_example(translator "" "${EXAMPLES_LINK_LIBS}" ""
+    # argument to binary (for testing)
+    ${CMAKE_CURRENT_SOURCE_DIR}/translator-example-input.smt2)
 
 if(BUILD_BINDINGS_JAVA)
   find_package(Java REQUIRED)
diff --git a/examples/sets-translate/sets-translate-example-input.smt2 b/examples/sets-translate/sets-translate-example-input.smt2
index 3bf1a9b6a..be230b113 100644
--- a/examples/sets-translate/sets-translate-example-input.smt2
+++ b/examples/sets-translate/sets-translate-example-input.smt2
@@ -1,5 +1,3 @@
-; COMMAND-LINE: --finite-model-find
-; EXPECT: sat
 (set-logic ALL)
 (declare-sort Atom 0)
 
diff --git a/examples/translator-example-input.smt2 b/examples/translator-example-input.smt2
new file mode 100644
index 000000000..be230b113
--- /dev/null
+++ b/examples/translator-example-input.smt2
@@ -0,0 +1,20 @@
+(set-logic ALL)
+(declare-sort Atom 0)
+
+(declare-fun k (Atom Atom) (Set Atom))
+
+(declare-fun t0 () Atom)
+(declare-fun t1 () Atom)
+(declare-fun t2 () Atom)
+(declare-fun v () Atom)
+(declare-fun b2 () Atom)
+
+(assert (forall ((b Atom)) (or 
+(member v (k t0 b))
+(member v (k t1 b))
+) ))
+
+(assert (not (member v (k t2 b2))))
+
+(check-sat)
+
-- 
2.30.2