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).

diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index 33d341ac893fd23bdb04223c978847808ad9fe3f..68eb06074bf1735fd031334794d7ce242f9890d6 100644 (file)
--- 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 3bf1a9b6afed272f303a16ab673a0a65ce36a023..be230b1136c3016331ae400a72bafda0961ef1e2 100644 (file)
--- 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 (file)
index 0000000..be230b1
--- /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)
+