From: Gereon Kremer <nafur42@gmail.com>
Date: Thu, 14 Oct 2021 23:38:21 +0000 (-0700)
Subject: Fix (get-info :authors) (#7373)
X-Git-Tag: cvc5-1.0.0~1062
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2e50a66e1cb58a86ff456948a6efff492487c21a;p=cvc5.git

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.
---

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")
   {