diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-10-08 17:34:35 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-08 17:34:35 -0700 |
commit | 55acdeb493ee3f9b66ed38f7526670b6e66c46bd (patch) | |
tree | 7e3ca116f1a243adc93083e5016f422cfb316680 /examples/translator-example-input.smt2 | |
parent | bd5f6d16dc88624a1dbf463f5d080bdc5af50494 (diff) |
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).
Diffstat (limited to 'examples/translator-example-input.smt2')
-rw-r--r-- | examples/translator-example-input.smt2 | 20 |
1 files changed, 20 insertions, 0 deletions
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) + |