From 219e2763d670e7bad8d6178fa4dd80b5bf1f6ea8 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 25 Mar 2022 14:19:35 -0500
Subject: [PATCH] Change output of abduction/interpolation for failed inputs
 (#8396)

Changes from "none" to "fail" to be consistent with SyGuS standard. Note that this means that we don't know if an abduct/interpolant exists.
---
 src/smt/command.cpp                                       | 8 ++++----
 .../regress1/abduction/issue5848-3-trivial-no-abduct.smt2 | 2 +-
 test/regress/cli/regress1/abduction/issue5848-4.smt2      | 2 +-
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 4222ef4a6..04dbc77bb 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1953,7 +1953,7 @@ void GetInterpolCommand::printResult(std::ostream& out) const
     }
     else
     {
-      out << "none" << std::endl;
+      out << "fail" << std::endl;
     }
   }
 }
@@ -2020,7 +2020,7 @@ void GetInterpolNextCommand::printResult(std::ostream& out) const
     }
     else
     {
-      out << "none" << std::endl;
+      out << "fail" << std::endl;
     }
   }
 }
@@ -2110,7 +2110,7 @@ void GetAbductCommand::printResult(std::ostream& out) const
     }
     else
     {
-      out << "none" << std::endl;
+      out << "fail" << std::endl;
     }
   }
 }
@@ -2173,7 +2173,7 @@ void GetAbductNextCommand::printResult(std::ostream& out) const
     }
     else
     {
-      out << "none" << std::endl;
+      out << "fail" << std::endl;
     }
   }
 }
diff --git a/test/regress/cli/regress1/abduction/issue5848-3-trivial-no-abduct.smt2 b/test/regress/cli/regress1/abduction/issue5848-3-trivial-no-abduct.smt2
index b64e27b45..bd2e379c7 100644
--- a/test/regress/cli/regress1/abduction/issue5848-3-trivial-no-abduct.smt2
+++ b/test/regress/cli/regress1/abduction/issue5848-3-trivial-no-abduct.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --produce-abducts
-; EXPECT: none
+; EXPECT: fail
 (set-logic ALL)
 (assert (= 0.0 (sqrt 1.0)))
 (get-abduct A false)
diff --git a/test/regress/cli/regress1/abduction/issue5848-4.smt2 b/test/regress/cli/regress1/abduction/issue5848-4.smt2
index 93cd8f52b..4bb4125a7 100644
--- a/test/regress/cli/regress1/abduction/issue5848-4.smt2
+++ b/test/regress/cli/regress1/abduction/issue5848-4.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --produce-abducts
-; EXPECT: none
+; EXPECT: fail
 (set-logic UFLRA)
 (declare-sort S0 0)
 (declare-fun S0-0 () S0)
-- 
2.30.2