From 2e50a66e1cb58a86ff456948a6efff492487c21a Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 14 Oct 2021 16:38:21 -0700 Subject: [PATCH] Fix (get-info :authors) (#7373) This PR fixes calling (get-info :authors). It used to (try to) print the whole about() information, but failed to do so because the string needed to be turned into an s-expression. However, about() is not properly escaped. We now simply print the cvc5 authors. It also fixes isValidGetInfoFlag() which was missing filename. Fixes #7362. --- src/smt/solver_engine.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 911e0a960..e928dcade 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -417,10 +417,10 @@ void SolverEngine::setInfo(const std::string& key, const std::string& value) bool SolverEngine::isValidGetInfoFlag(const std::string& key) const { - if (key == "all-statistics" || key == "error-behavior" || key == "name" - || key == "version" || key == "authors" || key == "status" - || key == "reason-unknown" || key == "assertion-stack-levels" - || key == "all-options" || key == "time") + if (key == "all-statistics" || key == "error-behavior" || key == "filename" + || key == "name" || key == "version" || key == "authors" + || key == "status" || key == "time" || key == "reason-unknown" + || key == "assertion-stack-levels" || key == "all-options") { return true; } @@ -455,7 +455,7 @@ std::string SolverEngine::getInfo(const std::string& key) const } if (key == "authors") { - return toSExpr(Configuration::about()); + return toSExpr("the " + Configuration::getName() + " authors"); } if (key == "status") { -- 2.30.2