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.

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 4222ef4a6b3d98507813a37c74ee8ef7c5b95992..04dbc77bbca08dd73b2f2fca1134aab715c75fea 100644 (file)
--- 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 b64e27b45593530a1a818e1f1a76933c079765e6..bd2e379c722bb3151668bb372d07cd0042dcbc4e 100644 (file)
--- 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 93cd8f52bbc4b203e7418a9ec632f121d31a489a..4bb4125a7044466484c8949b3c4ff7517f4b8a51 100644 (file)
--- 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)