From ae5ee4b07dc3d3c792e7fe7f382ff490dd28aca4 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Wed, 21 Apr 2021 10:21:34 -0700 Subject: Goodbye CVC4, hello cvc5! (#6371) This commits changes the build system to cvc5 and removes the remaining occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/. --- examples/simple_vc_quant_cxx.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'examples/simple_vc_quant_cxx.cpp') diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp index 9ef48bf76..1bdadfca2 100644 --- a/examples/simple_vc_quant_cxx.cpp +++ b/examples/simple_vc_quant_cxx.cpp @@ -48,10 +48,10 @@ int main() { slv.assertFormula(formula); - std::cout << "Checking SAT after asserting " << formula << " to CVC4." + std::cout << "Checking SAT after asserting " << formula << " to cvc5." << std::endl; - std::cout << "CVC4 should report unsat." << std::endl; - std::cout << "Result from CVC4 is: " << slv.checkSat() << std::endl; + std::cout << "cvc5 should report unsat." << std::endl; + std::cout << "Result from cvc5 is: " << slv.checkSat() << std::endl; slv.resetAssertions(); @@ -66,10 +66,10 @@ int main() { slv.assertFormula(formula_pattern); - std::cout << "Checking SAT after asserting " << formula_pattern << " to CVC4." + std::cout << "Checking SAT after asserting " << formula_pattern << " to cvc5." << std::endl; - std::cout << "CVC4 should report unsat." << std::endl; - std::cout << "Result from CVC4 is: " << slv.checkSat() << std::endl; + std::cout << "cvc5 should report unsat." << std::endl; + std::cout << "Result from cvc5 is: " << slv.checkSat() << std::endl; return 0; } -- cgit v1.2.3