Commit 80a6dadc authored by Fabian Wolff's avatar Fabian Wolff

Add hello-world test in debian/tests/

parent cd4918e9
......@@ -44,7 +44,8 @@ Section: libdevel
Depends: libcvc4-4 (= ${binary:Version}),
libcvc4parser4 (= ${binary:Version}),
${shlibs:Depends},
${misc:Depends}
${misc:Depends},
libgmp-dev
Description: automated theorem prover for SMT problems (development files)
CVC4 is an efficient automatic theorem prover for satisfiability
modulo theories (SMT) problems. It can be used to prove the validity
......
Tests: hello-world
Depends: @, build-essential
#!/bin/sh
set -e
TMPDIR=$(mktemp -d)
trap "rm -rf $TMPDIR" EXIT
cd $TMPDIR
cat <<EOF > hello-world.cc
#include <iostream>
#include <cvc4/cvc4.h>
using namespace CVC4;
int main ()
{
ExprManager em;
Expr helloWorld = em.mkVar ("Hello world!", em.booleanType ());
SmtEngine smt (&em);
std::cout << helloWorld << " is " << smt.query (helloWorld) << std::endl;
return 0;
}
EOF
c++ -o hello-world hello-world.cc -lcvc4 -Wno-deprecated
[ -x hello-world ]
./hello-world > output
echo "Hello world! is invalid" > expected
diff expected output
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment