diff options
Diffstat (limited to 'examples/api/cpp/bitvectors_and_arrays.cpp')
-rw-r--r-- | examples/api/cpp/bitvectors_and_arrays.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
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; |