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 <cvc5/cvc5.h>
using namespace cvc5;
int main ()
{
TermManager tm;
Term helloworld = tm.mkConst(tm.getBooleanSort(), "Hello World!");
std::cout << helloworld << " is " << Solver{tm}.checkSatAssuming(helloworld)
<< std::endl;
return 0;
}
EOF
c++ -o hello-world hello-world.cc -lcvc5
[ -x hello-world ]
./hello-world > output
echo "|Hello World!| is sat" > expected
diff expected output
|
