From 59bbcb5aa51b2ae9689e69afb05b017ee4fcb43a Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Tue, 15 Jun 2021 15:29:08 -0300 Subject: CVC4 -> cvc5 in cpp API examples (#6746) --- examples/api/cpp/bitvectors_and_arrays.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'examples/api/cpp/bitvectors_and_arrays.cpp') diff --git a/examples/api/cpp/bitvectors_and_arrays.cpp b/examples/api/cpp/bitvectors_and_arrays.cpp index 547b294a0..6b58daf1b 100644 --- a/examples/api/cpp/bitvectors_and_arrays.cpp +++ b/examples/api/cpp/bitvectors_and_arrays.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * A simple demonstration of the solving capabilities of the CVC4 + * A simple demonstration of the solving capabilities of the cvc5 * bit-vector and array solvers. * */ @@ -84,10 +84,10 @@ int main() Term query = slv.mkTerm(NOT, slv.mkTerm(AND, assertions)); - cout << "Asserting " << query << " to CVC4 " << endl; + cout << "Asserting " << query << " to cvc5 " << endl; slv.assertFormula(query); cout << "Expect sat. " << endl; - cout << "CVC4: " << slv.checkSatAssuming(slv.mkTrue()) << endl; + cout << "cvc5: " << slv.checkSatAssuming(slv.mkTrue()) << endl; // Getting the model cout << "The satisfying model is: " << endl; -- cgit v1.2.3