1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
#!/bin/sh
set -e
TMPDIR=$(mktemp -d)
trap "rm -rf $TMPDIR" EXIT
cd $TMPDIR
cat <<EOF > hello-world.cc
#include <iostream>
#include <cvc4/api/cvc4cpp.h>
using namespace CVC4::api;
int main ()
{
Solver slv;
Term helloworld = slv.mkVar(slv.getBooleanSort(), "Hello World!");
std::cout << helloworld << " is " << slv.checkEntailed(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 not_entailed" > expected
diff expected output
|
