From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 11 Mar 2022 21:41:54 +0000 (-0600)
Subject: Update abduction and interpolation API to not use pass/return by reference (#8263)
X-Git-Tag: cvc5-1.0.0~275
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5278d7deb81773f8a801966f7aa7e8475efa5d84;p=cvc5.git

Update abduction and interpolation API to not use pass/return by reference (#8263)
---

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index c65db3dd1..a54588b11 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7563,7 +7563,7 @@ void Solver::pop(uint32_t nscopes) const
   CVC5_API_TRY_CATCH_END;
 }
 
-bool Solver::getInterpolant(const Term& conj, Term& output) const
+Term Solver::getInterpolant(const Term& conj) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(conj);
@@ -7572,21 +7572,14 @@ bool Solver::getInterpolant(const Term& conj, Term& output) const
       << "Cannot get interpolant unless interpolants are enabled (try "
          "--produce-interpols=mode)";
   //////// all checks before this line
-  Node result;
   TypeNode nullType;
-  bool success = d_slv->getInterpolant(*conj.d_node, nullType, result);
-  if (success)
-  {
-    output = Term(this, result);
-  }
-  return success;
+  Node result = d_slv->getInterpolant(*conj.d_node, nullType);
+  return Term(this, result);
   ////////
   CVC5_API_TRY_CATCH_END;
 }
 
-bool Solver::getInterpolant(const Term& conj,
-                            Grammar& grammar,
-                            Term& output) const
+Term Solver::getInterpolant(const Term& conj, Grammar& grammar) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(conj);
@@ -7595,19 +7588,13 @@ bool Solver::getInterpolant(const Term& conj,
       << "Cannot get interpolant unless interpolants are enabled (try "
          "--produce-interpols=mode)";
   //////// all checks before this line
-  Node result;
-  bool success =
-      d_slv->getInterpolant(*conj.d_node, *grammar.resolve().d_type, result);
-  if (success)
-  {
-    output = Term(this, result);
-  }
-  return success;
+  Node result = d_slv->getInterpolant(*conj.d_node, *grammar.resolve().d_type);
+  return Term(this, result);
   ////////
   CVC5_API_TRY_CATCH_END;
 }
 
-bool Solver::getInterpolantNext(Term& output) const
+Term Solver::getInterpolantNext() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK(d_slv->getOptions().smt.produceInterpols
@@ -7618,56 +7605,40 @@ bool Solver::getInterpolantNext(Term& output) const
       << "Cannot get next interpolant when not solving incrementally (try "
          "--incremental)";
   //////// all checks before this line
-  Node result;
-  bool success = d_slv->getInterpolantNext(result);
-  if (success)
-  {
-    output = Term(this, result);
-  }
-  return success;
+  Node result = d_slv->getInterpolantNext();
+  return Term(this, result);
   ////////
   CVC5_API_TRY_CATCH_END;
 }
 
-bool Solver::getAbduct(const Term& conj, Term& output) const
+Term Solver::getAbduct(const Term& conj) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(conj);
   CVC5_API_CHECK(d_slv->getOptions().smt.produceAbducts)
       << "Cannot get abduct unless abducts are enabled (try --produce-abducts)";
   //////// all checks before this line
-  Node result;
   TypeNode nullType;
-  bool success = d_slv->getAbduct(*conj.d_node, nullType, result);
-  if (success)
-  {
-    output = Term(this, result);
-  }
-  return success;
+  Node result = d_slv->getAbduct(*conj.d_node, nullType);
+  return Term(this, result);
   ////////
   CVC5_API_TRY_CATCH_END;
 }
 
-bool Solver::getAbduct(const Term& conj, Grammar& grammar, Term& output) const
+Term Solver::getAbduct(const Term& conj, Grammar& grammar) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(conj);
   CVC5_API_CHECK(d_slv->getOptions().smt.produceAbducts)
       << "Cannot get abduct unless abducts are enabled (try --produce-abducts)";
   //////// all checks before this line
-  Node result;
-  bool success =
-      d_slv->getAbduct(*conj.d_node, *grammar.resolve().d_type, result);
-  if (success)
-  {
-    output = Term(this, result);
-  }
-  return success;
+  Node result = d_slv->getAbduct(*conj.d_node, *grammar.resolve().d_type);
+  return Term(this, result);
   ////////
   CVC5_API_TRY_CATCH_END;
 }
 
-bool Solver::getAbductNext(Term& output) const
+Term Solver::getAbductNext() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK(d_slv->getOptions().smt.produceAbducts)
@@ -7677,13 +7648,8 @@ bool Solver::getAbductNext(Term& output) const
       << "Cannot get next abduct when not solving incrementally (try "
          "--incremental)";
   //////// all checks before this line
-  Node result;
-  bool success = d_slv->getAbductNext(result);
-  if (success)
-  {
-    output = Term(this, result);
-  }
-  return success;
+  Node result = d_slv->getAbductNext();
+  return Term(this, result);
   ////////
   CVC5_API_TRY_CATCH_END;
 }
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 229fe6235..95c2d73b1 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -4422,11 +4422,11 @@ class CVC5_EXPORT Solver
    * \endverbatim
    *
    * @param conj the conjecture term
-   * @param output a Term I such that A->I and I->B are valid, where A is the
-   *        current set of assertions and B is given in the input by conj.
-   * @return true if it gets I successfully, false otherwise.
+   * @return a Term I such that A->I and I->B are valid, where A is the
+   *        current set of assertions and B is given in the input by conj,
+   *        or the null term if such a term cannot be found.
    */
-  bool getInterpolant(const Term& conj, Term& output) const;
+  Term getInterpolant(const Term& conj) const;
 
   /**
    * Get an interpolant
@@ -4445,11 +4445,11 @@ class CVC5_EXPORT Solver
    *
    * @param conj the conjecture term
    * @param grammar the grammar for the interpolant I
-   * @param output a Term I such that A->I and I->B are valid, where A is the
-   *        current set of assertions and B is given in the input by conj.
-   * @return true if it gets I successfully, false otherwise.
+   * @return a Term I such that A->I and I->B are valid, where A is the
+   *         current set of assertions and B is given in the input by conj,
+   *         or the null term if such a term cannot be found.
    */
-  bool getInterpolant(const Term& conj, Grammar& grammar, Term& output) const;
+  Term getInterpolant(const Term& conj, Grammar& grammar) const;
 
   /**
    * Get the next interpolant. Can only be called immediately after a successful
@@ -4469,12 +4469,11 @@ class CVC5_EXPORT Solver
    * mode different from `none`.
    * \endverbatim
    *
-   * @param output a Term I such that A->I and I->B are valid, where A is the
-   *        current set of assertions and B is given in the input by conj
-   *        on the last call to getInterpolant.
-   * @return true if it gets interpolant @f$C@f$ successfully, false otherwise
+   * @return a Term I such that A->I and I->B are valid, where A is the
+   *         current set of assertions and B is given in the input by conj
+   *         on the last call to getInterpolant.
    */
-  bool getInterpolantNext(Term& output) const;
+  Term getInterpolantNext() const;
 
   /**
    * Get an abduct.
@@ -4491,13 +4490,13 @@ class CVC5_EXPORT Solver
    * \endverbatim
    *
    * @param conj the conjecture term
-   * @param output a term @f$C@f$ such that @f$(A \wedge C)@f$ is satisfiable,
-   *               and @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where
-   *               @f$A@f$ is the current set of assertions and @f$B@f$ is
-   *               given in the input by ``conj``.
-   * @return true if it gets abduct @f$C@f$ successfully, false otherwise
+   * @return a term @f$C@f$ such that @f$(A \wedge C)@f$ is satisfiable,
+   *         and @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where
+   *         @f$A@f$ is the current set of assertions and @f$B@f$ is
+   *         given in the input by ``conj``, or the null term if such a term
+   *         cannot be found.
    */
-  bool getAbduct(const Term& conj, Term& output) const;
+  Term getAbduct(const Term& conj) const;
 
   /**
    * Get an abduct.
@@ -4515,13 +4514,12 @@ class CVC5_EXPORT Solver
    *
    * @param conj the conjecture term
    * @param grammar the grammar for the abduct @f$C@f$
-   * @param output a term C such that @f$(A \wedge C)@f$ is satisfiable, and
+   * @return a term C such that @f$(A \wedge C)@f$ is satisfiable, and
    *        @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where @f$A@f$ is
    *        the current set of assertions and @f$B@f$ is given in the input by
-   *        ``conj``
-   * @return true if it gets abduct @f$C@f$ successfully, false otherwise
+   *        ``conj``, or the null term if such a term cannot be found.
    */
-  bool getAbduct(const Term& conj, Grammar& grammar, Term& output) const;
+  Term getAbduct(const Term& conj, Grammar& grammar) const;
 
   /**
    * Get the next abduct. Can only be called immediately after a successful
@@ -4539,13 +4537,13 @@ class CVC5_EXPORT Solver
    * :ref:`produce-abducts <lbl-option-produce-abducts>`.
    * \endverbatim
    *
-   * @param output a term C such that @f$(A \wedge C)@f$ is satisfiable, and
+   * @return a term C such that @f$(A \wedge C)@f$ is satisfiable, and
    *        @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where @f$A@f$ is
    *        the current set of assertions and @f$B@f$ is given in the input by
-   *        the last call to getAbduct.
-   * @return true if it gets abduct @f$C@f$ successfully, false otherwise
+   *        the last call to getAbduct, or the null term if such a term cannot
+   *        be found.
    */
-  bool getAbductNext(Term& output) const;
+  Term getAbductNext() const;
 
   /**
    * Block the current model. Can be called only if immediately preceded by a
diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java
index 62e6d94eb..5b985c4cb 100644
--- a/src/api/java/io/github/cvc5/api/Solver.java
+++ b/src/api/java/io/github/cvc5/api/Solver.java
@@ -2166,16 +2166,17 @@ public class Solver implements IPointer, AutoCloseable
    * }
    * Requires 'produce-interpols' to be set to a mode different from 'none'.
    * @param conj the conjecture term
-   * @param output a Term I such that {@code A->I} and {@code I->B} are valid, where A is the
-   *        current set of assertions and B is given in the input by conj.
-   * @return true if it gets I successfully, false otherwise.
+   * @return a Term I such that {@code A->I} and {@code I->B} are valid, where
+   *        A is the current set of assertions and B is given in the input by
+   *        conj, or the null term if such a term cannot be found.
    */
-  public boolean getInterpolant(Term conj, Term output)
+  public Term getInterpolant(Term conj)
   {
-    return getInterpolant(pointer, conj.getPointer(), output.getPointer());
+    long interpolPtr = getInterpolant(pointer, conj.getPointer());
+    return new Term(this, interpolPtr);
   }
 
-  private native boolean getInterpolant(long pointer, long conjPointer, long outputPointer);
+  private native long getInterpolant(long pointer, long conjPointer);
 
   /**
    * Get an interpolant
@@ -2186,17 +2187,17 @@ public class Solver implements IPointer, AutoCloseable
    * Requires 'produce-interpols' to be set to a mode different from 'none'.
    * @param conj the conjecture term
    * @param grammar the grammar for the interpolant I
-   * @param output a Term I such that {@code A->I} and {@code I->B} are valid, where A is the
-   *        current set of assertions and B is given in the input by conj.
-   * @return true if it gets I successfully, false otherwise.
+   * @return a Term I such that {@code A->I} and {@code I->B} are valid, where
+   *        A is the current set of assertions and B is given in the input by
+   *        conj, or the null term if such a term cannot be found.
    */
-  public boolean getInterpolant(Term conj, Grammar grammar, Term output)
+  public Term getInterpolant(Term conj, Grammar grammar)
   {
-    return getInterpolant(pointer, conj.getPointer(), grammar.getPointer(), output.getPointer());
+    long interpolPtr = getInterpolant(pointer, conj.getPointer(), grammar.getPointer());
+    return new Term(this, interpolPtr);
   }
 
-  private native boolean getInterpolant(
-      long pointer, long conjPointer, long grammarPointer, long outputPointer);
+  private native long getInterpolant(long pointer, long conjPointer, long grammarPointer);
 
   /**
    * Get the next interpolant. Can only be called immediately after a successful
@@ -2215,17 +2216,18 @@ public class Solver implements IPointer, AutoCloseable
    * set to a mode different from 'none'.
    * \endverbatim
    *
-   * @param output a Term I such that {@code A->I} and {@code I->B} are valid,
+   * @return a Term I such that {@code A->I} and {@code I->B} are valid,
    *        where A is the current set of assertions and B is given in the input
-   *        by conj on the last call to getInterpolant.
-   * @return true if it gets interpolant @f$C@f$ successfully, false otherwise
+   *        by conj on the last call to getInterpolant, or the null term if such
+   *        a term cannot be found.
    */
-  public boolean getInterpolantNext(Term output)
+  public Term getInterpolantNext()
   {
-    return getInterpolantNext(pointer, output.getPointer());
+    long interpolPtr = getInterpolantNext(pointer);
+    return new Term(this, interpolPtr);
   }
 
-  private native boolean getInterpolantNext(long pointer, long outputPointer);
+  private native long getInterpolantNext(long pointer);
 
   /**
    * Get an abduct.
@@ -2235,17 +2237,18 @@ public class Solver implements IPointer, AutoCloseable
    * }
    * Requires enabling option 'produce-abducts'
    * @param conj the conjecture term
-   * @param output a term C such that A^C is satisfiable, and A^~B^C is
+   * @return a term C such that A^C is satisfiable, and A^~B^C is
    *        unsatisfiable, where A is the current set of assertions and B is
-   *        given in the input by conj
-   * @return true if it gets C successfully, false otherwise
+   *        given in the input by conj, or the null term if such a term cannot
+   *        be found.
    */
-  public boolean getAbduct(Term conj, Term output)
+  public Term getAbduct(Term conj)
   {
-    return getAbduct(pointer, conj.getPointer(), output.getPointer());
+    long abdPtr = getAbduct(pointer, conj.getPointer());
+    return new Term(this, abdPtr);
   }
 
-  private native boolean getAbduct(long pointer, long conjPointer, long outputPointer);
+  private native long getAbduct(long pointer, long conjPointer);
   /**
    * Get an abduct.
    * SMT-LIB:
@@ -2255,18 +2258,18 @@ public class Solver implements IPointer, AutoCloseable
    * Requires enabling option 'produce-abducts'
    * @param conj the conjecture term
    * @param grammar the grammar for the abduct C
-   * @param output a term C such that A^C is satisfiable, and A^~B^C is
+   * @return a term C such that A^C is satisfiable, and A^~B^C is
    *        unsatisfiable, where A is the current set of assertions and B is
-   *        given in the input by conj
-   * @return true if it gets C successfully, false otherwise
+   *        given in the input by conj, or the null term if such a term cannot
+   *        be found.
    */
-  public boolean getAbduct(Term conj, Grammar grammar, Term output)
+  public Term getAbduct(Term conj, Grammar grammar)
   {
-    return getAbduct(pointer, conj.getPointer(), grammar.getPointer(), output.getPointer());
+    long abdPtr = getAbduct(pointer, conj.getPointer(), grammar.getPointer());
+    return new Term(this, abdPtr);
   }
 
-  private native boolean getAbduct(
-      long pointer, long conjPointer, long grammarPointer, long outputPointer);
+  private native long getAbduct(long pointer, long conjPointer, long grammarPointer);
 
   /**
    * Get the next abduct. Can only be called immediately after a successful
@@ -2277,16 +2280,18 @@ public class Solver implements IPointer, AutoCloseable
    * ( get-abduct-next )
    * }
    * Requires enabling incremental mode and option 'produce-abducts'
-   * @param output a term C such that A^C is satisfiable, and A^~B^C is
-   *        unsatisfiable, where A is the current set of assertions and B is
-   *        given in the input by conj in the last call to getAbduct.
-   * @return true if it gets C successfully, false otherwise
+   * @return a term C such that A^C is satisfiable, and A^~B^C is
+   *         unsatisfiable, where A is the current set of assertions and B is
+   *         given in the input by conj in the last call to getAbduct, or the
+   *         null term if such a term cannot be found.
    */
-  public boolean getAbductNext(Term output) {
-    return getAbductNext(pointer, output.getPointer());
+  public Term getAbductNext()
+  {
+    long abdPtr = getAbductNext(pointer);
+    return new Term(this, abdPtr);
   }
 
-  private native boolean getAbductNext(long pointer, long outputPointer);
+  private native long getAbductNext(long pointer);
 
   /**
    * Block the current model. Can be called only if immediately preceded by a
diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp
index 63a6c179a..7d4d2acd6 100644
--- a/src/api/java/jni/solver.cpp
+++ b/src/api/java/jni/solver.cpp
@@ -2178,106 +2178,104 @@ JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_pop(JNIEnv* env,
 /*
  * Class:     io_github_cvc5_api_Solver
  * Method:    getInterpolant
- * Signature: (JJJ)Z
+ * Signature: (JJ)J
  */
-JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Solver_getInterpolant__JJJ(
-    JNIEnv* env, jobject, jlong pointer, jlong conjPointer, jlong outputPointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getInterpolant__JJ(
+    JNIEnv* env, jobject, jlong pointer, jlong conjPointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
   Term* conj = reinterpret_cast<Term*>(conjPointer);
-  Term* output = reinterpret_cast<Term*>(outputPointer);
-  return (jboolean)solver->getInterpolant(*conj, *output);
+  Term* result = new Term(solver->getInterpolant(*conj));
+  return reinterpret_cast<jlong>(result);
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
 /*
  * Class:     io_github_cvc5_api_Solver
  * Method:    getInterpolant
- * Signature: (JJJJ)Z
+ * Signature: (JJJ)J
  */
-JNIEXPORT jboolean JNICALL
-Java_io_github_cvc5_api_Solver_getInterpolant__JJJJ(JNIEnv* env,
-                                                    jobject,
-                                                    jlong pointer,
-                                                    jlong conjPointer,
-                                                    jlong grammarPointer,
-                                                    jlong outputPointer)
+JNIEXPORT jlong JNICALL
+Java_io_github_cvc5_api_Solver_getInterpolant__JJJ(JNIEnv* env,
+                                                   jobject,
+                                                   jlong pointer,
+                                                   jlong conjPointer,
+                                                   jlong grammarPointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
   Term* conj = reinterpret_cast<Term*>(conjPointer);
   Grammar* grammar = reinterpret_cast<Grammar*>(grammarPointer);
-  Term* output = reinterpret_cast<Term*>(outputPointer);
-  return (jboolean)solver->getInterpolant(*conj, *grammar, *output);
+  Term* result = new Term(solver->getInterpolant(*conj, *grammar));
+  return reinterpret_cast<jlong>(result);
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
 /*
  * Class:     io_github_cvc5_api_Solver
  * Method:    getInterpolantNext
- * Signature: (JJ)Z
+ * Signature: (J)J
  */
-JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Solver_getInterpolantNext(
-    JNIEnv* env, jobject, jlong pointer, jlong outputPointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getInterpolantNext(
+    JNIEnv* env, jobject, jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
-  Term* output = reinterpret_cast<Term*>(outputPointer);
-  return (jboolean)solver->getInterpolantNext(*output);
+  Term* result = new Term(solver->getInterpolantNext());
+  return reinterpret_cast<jlong>(result);
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
 /*
  * Class:     io_github_cvc5_api_Solver
  * Method:    getAbduct
- * Signature: (JJJ)Z
+ * Signature: (JJ)J
  */
-JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Solver_getAbduct__JJJ(
-    JNIEnv* env, jobject, jlong pointer, jlong conjPointer, jlong outputPointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getAbduct__JJ(
+    JNIEnv* env, jobject, jlong pointer, jlong conjPointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
   Term* conj = reinterpret_cast<Term*>(conjPointer);
-  Term* output = reinterpret_cast<Term*>(outputPointer);
-  return (jboolean)solver->getAbduct(*conj, *output);
+  Term* result = new Term(solver->getAbduct(*conj));
+  return reinterpret_cast<jlong>(result);
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
 /*
  * Class:     io_github_cvc5_api_Solver
  * Method:    getAbduct
- * Signature: (JJJJ)Z
+ * Signature: (JJJ)J
  */
-JNIEXPORT jboolean JNICALL
-Java_io_github_cvc5_api_Solver_getAbduct__JJJJ(JNIEnv* env,
-                                               jobject,
-                                               jlong pointer,
-                                               jlong conjPointer,
-                                               jlong grammarPointer,
-                                               jlong outputPointer)
+JNIEXPORT jlong JNICALL
+Java_io_github_cvc5_api_Solver_getAbduct__JJJ(JNIEnv* env,
+                                              jobject,
+                                              jlong pointer,
+                                              jlong conjPointer,
+                                              jlong grammarPointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
   Term* conj = reinterpret_cast<Term*>(conjPointer);
   Grammar* grammar = reinterpret_cast<Grammar*>(grammarPointer);
-  Term* output = reinterpret_cast<Term*>(outputPointer);
-  return (jboolean)solver->getAbduct(*conj, *grammar, *output);
+  Term* result = new Term(solver->getAbduct(*conj, *grammar));
+  return reinterpret_cast<jlong>(result);
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
 /*
  * Class:     io_github_cvc5_api_Solver
  * Method:    getAbductNext
- * Signature: (JJ)Z
+ * Signature: (J)J
  */
-JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Solver_getAbductNext
-    (JNIEnv * env, jobject, jlong pointer, jlong outputPointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getAbductNext(
+    JNIEnv* env, jobject, jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
-  Term* output = reinterpret_cast<Term*>(outputPointer);
-  return (jboolean)solver->getAbductNext(*output);
+  Term* result = new Term(solver->getAbductNext());
+  return reinterpret_cast<jlong>(result);
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index bff77fbce..740a58a03 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -295,12 +295,12 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         void setInfo(string& keyword, const string& value) except +
         void setLogic(const string& logic) except +
         void setOption(const string& option, const string& value) except +
-        bint getInterpolant(const Term& conj, Term& output) except +
-        bint getInterpolant(const Term& conj, Grammar& grammar, Term& output) except +
-        bint getInterpolantNext(const Term& conj) except +
-        bint getAbduct(const Term& conj, Term& output) except +
-        bint getAbduct(const Term& conj, Grammar& grammar, Term& output) except +
-        bint getAbductNext(const Term& conj) except +
+        Term getInterpolant(const Term& conj) except +
+        Term getInterpolant(const Term& conj, Grammar& grammar) except +
+        Term getInterpolantNext() except +
+        Term getAbduct(const Term& conj) except +
+        Term getAbduct(const Term& conj, Grammar& grammar) except +
+        Term getAbductNext() except +
         void blockModel() except +
         void blockModelValues(const vector[Term]& terms) except +
         string getInstantiations() except +
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 2c535b2e4..b259687b4 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -2246,6 +2246,7 @@ cdef class Solver:
         """
         self.csolver.setOption(option.encode(), value.encode())
 
+
     def getInterpolant(self, Term conj, *args):
         """Get an interpolant.
 
@@ -2260,27 +2261,25 @@ cdef class Solver:
 
         Supports the following variants:
 
-        - ``bool getInteprolant(Term conj, Term output)``
-        - ``bool getInteprolant(Term conj, Grammar grammar, Term output)``
+        - ``Term getInteprolant(Term conj)``
+        - ``Term getInteprolant(Term conj, Grammar grammar)``
         
         :param conj: the conjecture term
         :param output: the term where the result will be stored
         :param grammar: a grammar for the inteprolant
         :return: True iff an interpolant was found
         """
-        result = False
-        if len(args) == 1:
-            assert isinstance(args[0], Term)
-            result = self.csolver.getInterpolant(conj.cterm, (<Term ?> args[0]).cterm)
+        cdef Term result = Term(self)
+        if len(args) == 0:
+            result.cterm = self.csolver.getInterpolant(conj.cterm)
         else:
-            assert len(args) == 2
+            assert len(args) == 1
             assert isinstance(args[0], Grammar)
-            assert isinstance(args[1], Term)
-            result = self.csolver.getInterpolant(conj.cterm, (<Grammar ?> args[0]).cgrammar, (<Term ?> args[1]).cterm)
+            result.cterm = self.csolver.getInterpolant(conj.cterm, (<Grammar ?> args[0]).cgrammar)
         return result
 
 
-    def getInterpolantNext(self, Term output):
+    def getInterpolantNext(self):
         """
         Get the next interpolant. Can only be called immediately after
         a succesful call to get-interpol or get-interpol-next. 
@@ -2299,7 +2298,8 @@ cdef class Solver:
         :param output: the term where the result will be stored
         :return: True iff an interpolant was found
         """
-        result = self.csolver.getInterpolantNext(output.cterm)
+        cdef Term result = Term(self)
+        result.cterm = self.csolver.getInterpolantNext()
         return result
         
     def getAbduct(self, Term conj, *args):
@@ -2316,26 +2316,24 @@ cdef class Solver:
 
         Supports the following variants:
 
-        - ``bool getAbduct(Term conj, Term output)``
-        - ``bool getAbduct(Term conj, Grammar grammar, Term output)``
+        - ``Term getAbduct(Term conj)``
+        - ``Term getAbduct(Term conj, Grammar grammar)``
         
         :param conj: the conjecture term
         :param output: the term where the result will be stored
         :param grammar: a grammar for the abduct 
         :return: True iff an abduct was found
         """
-        result = False
-        if len(args) == 1:
-            assert isinstance(args[0], Term)
-            result = self.csolver.getAbduct(conj.cterm, (<Term ?> args[0]).cterm)
+        cdef Term result = Term(self)
+        if len(args) == 0:
+            result.cterm  = self.csolver.getAbduct(conj.cterm)
         else:
-            assert len(args) == 2
+            assert len(args) == 1
             assert isinstance(args[0], Grammar)
-            assert isinstance(args[1], Term)
-            result = self.csolver.getAbduct(conj.cterm, (<Grammar ?> args[0]).cgrammar, (<Term ?> args[1]).cterm)
+            result.cterm = self.csolver.getAbduct(conj.cterm, (<Grammar ?> args[0]).cgrammar)
         return result
 
-    def getAbductNext(self, Term output):
+    def getAbductNext(self):
         """
         Get the next abduct. Can only be called immediately after
         a succesful call to get-abduct or get-abduct-next. 
@@ -2353,7 +2351,8 @@ cdef class Solver:
         :param output: the term where the result will be stored
         :return: True iff an abduct was found
         """
-        result = self.csolver.getAbductNext(output.cterm)
+        cdef Term result = Term(self)
+        result.cterm  = self.csolver.getAbductNext()
         return result
 
     def blockModel(self):
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 2766c6510..1474ed240 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1944,16 +1944,13 @@ void GetInstantiationsCommand::toStream(std::ostream& out,
 /* -------------------------------------------------------------------------- */
 
 GetInterpolCommand::GetInterpolCommand(const std::string& name, api::Term conj)
-    : d_name(name),
-      d_conj(conj),
-      d_sygus_grammar(nullptr),
-      d_resultStatus(false)
+    : d_name(name), d_conj(conj), d_sygus_grammar(nullptr)
 {
 }
 GetInterpolCommand::GetInterpolCommand(const std::string& name,
                                        api::Term conj,
                                        api::Grammar* g)
-    : d_name(name), d_conj(conj), d_sygus_grammar(g), d_resultStatus(false)
+    : d_name(name), d_conj(conj), d_sygus_grammar(g)
 {
 }
 
@@ -1975,12 +1972,11 @@ void GetInterpolCommand::invoke(api::Solver* solver, SymbolManager* sm)
     sm->setLastSynthName(d_name);
     if (d_sygus_grammar == nullptr)
     {
-      d_resultStatus = solver->getInterpolant(d_conj, d_result);
+      d_result = solver->getInterpolant(d_conj);
     }
     else
     {
-      d_resultStatus =
-          solver->getInterpolant(d_conj, *d_sygus_grammar, d_result);
+      d_result = solver->getInterpolant(d_conj, *d_sygus_grammar);
     }
     d_commandStatus = CommandSuccess::instance();
   }
@@ -2000,7 +1996,7 @@ void GetInterpolCommand::printResult(std::ostream& out) const
   {
     options::ioutils::Scope scope(out);
     options::ioutils::applyDagThresh(out, 0);
-    if (d_resultStatus)
+    if (!d_result.isNull())
     {
       out << "(define-fun " << d_name << " () Bool " << d_result << ")"
           << std::endl;
@@ -2017,7 +2013,6 @@ Command* GetInterpolCommand::clone() const
   GetInterpolCommand* c =
       new GetInterpolCommand(d_name, d_conj, d_sygus_grammar);
   c->d_result = d_result;
-  c->d_resultStatus = d_resultStatus;
   return c;
 }
 
@@ -2039,7 +2034,7 @@ void GetInterpolCommand::toStream(std::ostream& out,
 /* class GetInterpolNextCommand */
 /* -------------------------------------------------------------------------- */
 
-GetInterpolNextCommand::GetInterpolNextCommand() : d_resultStatus(false) {}
+GetInterpolNextCommand::GetInterpolNextCommand() {}
 
 api::Term GetInterpolNextCommand::getResult() const { return d_result; }
 
@@ -2049,7 +2044,7 @@ void GetInterpolNextCommand::invoke(api::Solver* solver, SymbolManager* sm)
   {
     // Get the name of the interpolant from the symbol manager
     d_name = sm->getLastSynthName();
-    d_resultStatus = solver->getInterpolantNext(d_result);
+    d_result = solver->getInterpolantNext();
     d_commandStatus = CommandSuccess::instance();
   }
   catch (exception& e)
@@ -2068,7 +2063,7 @@ void GetInterpolNextCommand::printResult(std::ostream& out) const
   {
     options::ioutils::Scope scope(out);
     options::ioutils::applyDagThresh(out, 0);
-    if (d_resultStatus)
+    if (!d_result.isNull())
     {
       out << "(define-fun " << d_name << " () Bool " << d_result << ")"
           << std::endl;
@@ -2084,7 +2079,6 @@ Command* GetInterpolNextCommand::clone() const
 {
   GetInterpolNextCommand* c = new GetInterpolNextCommand;
   c->d_result = d_result;
-  c->d_resultStatus = d_resultStatus;
   return c;
 }
 
@@ -2106,16 +2100,13 @@ void GetInterpolNextCommand::toStream(std::ostream& out,
 /* -------------------------------------------------------------------------- */
 
 GetAbductCommand::GetAbductCommand(const std::string& name, api::Term conj)
-    : d_name(name),
-      d_conj(conj),
-      d_sygus_grammar(nullptr),
-      d_resultStatus(false)
+    : d_name(name), d_conj(conj), d_sygus_grammar(nullptr)
 {
 }
 GetAbductCommand::GetAbductCommand(const std::string& name,
                                    api::Term conj,
                                    api::Grammar* g)
-    : d_name(name), d_conj(conj), d_sygus_grammar(g), d_resultStatus(false)
+    : d_name(name), d_conj(conj), d_sygus_grammar(g)
 {
 }
 
@@ -2138,11 +2129,11 @@ void GetAbductCommand::invoke(api::Solver* solver, SymbolManager* sm)
     sm->setLastSynthName(d_name);
     if (d_sygus_grammar == nullptr)
     {
-      d_resultStatus = solver->getAbduct(d_conj, d_result);
+      d_result = solver->getAbduct(d_conj);
     }
     else
     {
-      d_resultStatus = solver->getAbduct(d_conj, *d_sygus_grammar, d_result);
+      d_result = solver->getAbduct(d_conj, *d_sygus_grammar);
     }
     d_commandStatus = CommandSuccess::instance();
   }
@@ -2162,7 +2153,7 @@ void GetAbductCommand::printResult(std::ostream& out) const
   {
     options::ioutils::Scope scope(out);
     options::ioutils::applyDagThresh(out, 0);
-    if (d_resultStatus)
+    if (!d_result.isNull())
     {
       out << "(define-fun " << d_name << " () Bool " << d_result << ")"
           << std::endl;
@@ -2178,7 +2169,6 @@ Command* GetAbductCommand::clone() const
 {
   GetAbductCommand* c = new GetAbductCommand(d_name, d_conj, d_sygus_grammar);
   c->d_result = d_result;
-  c->d_resultStatus = d_resultStatus;
   return c;
 }
 
@@ -2197,7 +2187,7 @@ void GetAbductCommand::toStream(std::ostream& out,
 /* class GetAbductNextCommand */
 /* -------------------------------------------------------------------------- */
 
-GetAbductNextCommand::GetAbductNextCommand() : d_resultStatus(false) {}
+GetAbductNextCommand::GetAbductNextCommand() {}
 
 api::Term GetAbductNextCommand::getResult() const { return d_result; }
 
@@ -2207,7 +2197,7 @@ void GetAbductNextCommand::invoke(api::Solver* solver, SymbolManager* sm)
   {
     // Get the name of the abduct from the symbol manager
     d_name = sm->getLastSynthName();
-    d_resultStatus = solver->getAbductNext(d_result);
+    d_result = solver->getAbductNext();
     d_commandStatus = CommandSuccess::instance();
   }
   catch (exception& e)
@@ -2226,7 +2216,7 @@ void GetAbductNextCommand::printResult(std::ostream& out) const
   {
     options::ioutils::Scope scope(out);
     options::ioutils::applyDagThresh(out, 0);
-    if (d_resultStatus)
+    if (!d_result.isNull())
     {
       out << "(define-fun " << d_name << " () Bool " << d_result << ")"
           << std::endl;
@@ -2242,7 +2232,6 @@ Command* GetAbductNextCommand::clone() const
 {
   GetAbductNextCommand* c = new GetAbductNextCommand;
   c->d_result = d_result;
-  c->d_resultStatus = d_resultStatus;
   return c;
 }
 
diff --git a/src/smt/command.h b/src/smt/command.h
index b250d0b59..66c678ba8 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -1052,8 +1052,6 @@ class CVC5_EXPORT GetInterpolCommand : public Command
   api::Term d_conj;
   /** The (optional) grammar of the interpolation query */
   api::Grammar* d_sygus_grammar;
-  /** the return status of the command */
-  bool d_resultStatus;
   /** the return expression of the command */
   api::Term d_result;
 }; /* class GetInterpolCommand */
@@ -1081,8 +1079,6 @@ class CVC5_EXPORT GetInterpolNextCommand : public Command
  protected:
   /** The name of the interpolation predicate */
   std::string d_name;
-  /** the return status of the command */
-  bool d_resultStatus;
   /** the return expression of the command */
   api::Term d_result;
 };
@@ -1131,8 +1127,6 @@ class CVC5_EXPORT GetAbductCommand : public Command
   api::Term d_conj;
   /** The (optional) grammar of the abduction query */
   api::Grammar* d_sygus_grammar;
-  /** the return status of the command */
-  bool d_resultStatus;
   /** the return expression of the command */
   api::Term d_result;
 }; /* class GetAbductCommand */
@@ -1159,8 +1153,6 @@ class CVC5_EXPORT GetAbductNextCommand : public Command
  protected:
   /** The name of the abduction predicate */
   std::string d_name;
-  /** the return status of the command */
-  bool d_resultStatus;
   /** the return expression of the command */
   api::Term d_result;
 };
diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 583eaae7b..9d8311392 100644
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -1666,22 +1666,22 @@ Node SolverEngine::getQuantifierElimination(Node q, bool doFull)
       *d_asserts, q, doFull, d_isInternalSubsolver);
 }
 
-bool SolverEngine::getInterpolant(const Node& conj,
-                                  const TypeNode& grammarType,
-                                  Node& interpol)
+Node SolverEngine::getInterpolant(const Node& conj, const TypeNode& grammarType)
 {
   SolverEngineScope smts(this);
   finishInit();
   std::vector<Node> axioms = getExpandedAssertions();
+  Node interpol;
   bool success =
       d_interpolSolver->getInterpolant(axioms, conj, grammarType, interpol);
   // notify the state of whether the get-interpol call was successfuly, which
   // impacts the SMT mode.
   d_state->notifyGetInterpol(success);
-  return success;
+  Assert(success == !interpol.isNull());
+  return interpol;
 }
 
-bool SolverEngine::getInterpolantNext(Node& interpol)
+Node SolverEngine::getInterpolantNext()
 {
   SolverEngineScope smts(this);
   finishInit();
@@ -1691,27 +1691,29 @@ bool SolverEngine::getInterpolantNext(Node& interpol)
         "Cannot get-interpol-next unless immediately preceded by a successful "
         "call to get-interpol(-next).");
   }
+  Node interpol;
   bool success = d_interpolSolver->getInterpolantNext(interpol);
   // notify the state of whether the get-interpolant-next call was successful
   d_state->notifyGetInterpol(success);
-  return success;
+  Assert(success == !interpol.isNull());
+  return interpol;
 }
 
-bool SolverEngine::getAbduct(const Node& conj,
-                             const TypeNode& grammarType,
-                             Node& abd)
+Node SolverEngine::getAbduct(const Node& conj, const TypeNode& grammarType)
 {
   SolverEngineScope smts(this);
   finishInit();
   std::vector<Node> axioms = getExpandedAssertions();
+  Node abd;
   bool success = d_abductSolver->getAbduct(axioms, conj, grammarType, abd);
   // notify the state of whether the get-abduct call was successful, which
   // impacts the SMT mode.
   d_state->notifyGetAbduct(success);
-  return success;
+  Assert(success == !abd.isNull());
+  return abd;
 }
 
-bool SolverEngine::getAbductNext(Node& abd)
+Node SolverEngine::getAbductNext()
 {
   SolverEngineScope smts(this);
   finishInit();
@@ -1721,10 +1723,12 @@ bool SolverEngine::getAbductNext(Node& abd)
         "Cannot get-abduct-next unless immediately preceded by a successful "
         "call to get-abduct(-next).");
   }
+  Node abd;
   bool success = d_abductSolver->getAbductNext(abd);
   // notify the state of whether the get-abduct-next call was successful
   d_state->notifyGetAbduct(success);
-  return success;
+  Assert(success == !abd.isNull());
+  return abd;
 }
 
 void SolverEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h
index c6cd77dd7..ae8013965 100644
--- a/src/smt/solver_engine.h
+++ b/src/smt/solver_engine.h
@@ -639,18 +639,15 @@ class CVC5_EXPORT SolverEngine
    * This method invokes a separate copy of the SMT engine for solving the
    * corresponding sygus problem for generating such a solution.
    */
-  bool getInterpolant(const Node& conj,
-                      const TypeNode& grammarType,
-                      Node& interpol);
+  Node getInterpolant(const Node& conj, const TypeNode& grammarType);
 
   /**
    * Get next interpolant. This can only be called immediately after a
    * successful call to getInterpolant or getInterpolantNext.
    *
-   * Returns true if an interpolant was found, and sets interpol to the
-   * interpolant.
+   * Returns the interpolant if one exists, or the null node otherwise.
    */
-  bool getInterpolantNext(Node& interpol);
+  Node getInterpolantNext();
 
   /**
    * This method asks this SMT engine to find an abduct with respect to the
@@ -664,15 +661,15 @@ class CVC5_EXPORT SolverEngine
    * This method invokes a separate copy of the SMT engine for solving the
    * corresponding sygus problem for generating such a solution.
    */
-  bool getAbduct(const Node& conj, const TypeNode& grammarType, Node& abd);
+  Node getAbduct(const Node& conj, const TypeNode& grammarType);
 
   /**
    * Get next abduct. This can only be called immediately after a successful
    * call to getAbduct or getAbductNext.
    *
-   * Returns true if an abduct was found, and sets abd to the abduct.
+   * Returns the abduct if one exists, or the null node otherwise.
    */
-  bool getAbductNext(Node& abd);
+  Node getAbductNext();
 
   /**
    * Get list of quantified formulas that were instantiated on the last call
diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index d057154fc..4ea0b7ff1 100644
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -1343,9 +1343,8 @@ TEST_F(TestApiBlackSolver, getAbduct)
   d_solver.assertFormula(d_solver.mkTerm(GT, x, zero));
   // Conjecture for abduction: y > 0
   Term conj = d_solver.mkTerm(GT, y, zero);
-  Term output;
   // Call the abduction api, while the resulting abduct is the output
-  ASSERT_TRUE(d_solver.getAbduct(conj, output));
+  Term output = d_solver.getAbduct(conj);
   // We expect the resulting output to be a boolean formula
   ASSERT_TRUE(!output.isNull() && output.getSort().isBoolean());
 
@@ -1358,7 +1357,7 @@ TEST_F(TestApiBlackSolver, getAbduct)
   Term conj2 = d_solver.mkTerm(GT, x, zero);
   ASSERT_NO_THROW(g.addRule(start, truen));
   // Call the abduction api, while the resulting abduct is the output
-  ASSERT_TRUE(d_solver.getAbduct(conj2, g, output2));
+  output2 = d_solver.getAbduct(conj2, g);
   // abduct must be true
   ASSERT_EQ(output2, truen);
 }
@@ -1375,9 +1374,8 @@ TEST_F(TestApiBlackSolver, getAbduct2)
   d_solver.assertFormula(d_solver.mkTerm(GT, x, zero));
   // Conjecture for abduction: y > 0
   Term conj = d_solver.mkTerm(GT, y, zero);
-  Term output;
   // Fails due to option not set
-  ASSERT_THROW(d_solver.getAbduct(conj, output), CVC5ApiException);
+  ASSERT_THROW(d_solver.getAbduct(conj), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, getAbductNext)
@@ -1395,11 +1393,9 @@ TEST_F(TestApiBlackSolver, getAbductNext)
   d_solver.assertFormula(d_solver.mkTerm(GT, x, zero));
   // Conjecture for abduction: y > 0
   Term conj = d_solver.mkTerm(GT, y, zero);
-  Term output;
   // Call the abduction api, while the resulting abduct is the output
-  ASSERT_TRUE(d_solver.getAbduct(conj, output));
-  Term output2;
-  ASSERT_TRUE(d_solver.getAbductNext(output2));
+  Term output = d_solver.getAbduct(conj);
+  Term output2 = d_solver.getAbductNext();
   // should produce a different output
   ASSERT_TRUE(output != output2);
 }
@@ -1424,9 +1420,8 @@ TEST_F(TestApiBlackSolver, getInterpolant)
       d_solver.mkTerm(OR,
                       d_solver.mkTerm(GT, d_solver.mkTerm(ADD, y, z), zero),
                       d_solver.mkTerm(LT, z, zero));
-  Term output;
   // Call the interpolation api, while the resulting interpolant is the output
-  d_solver.getInterpolant(conj, output);
+  Term output = d_solver.getInterpolant(conj);
 
   // We expect the resulting output to be a boolean formula
   ASSERT_TRUE(output.getSort().isBoolean());
@@ -1451,10 +1446,8 @@ TEST_F(TestApiBlackSolver, getInterpolantNext)
       d_solver.mkTerm(OR,
                       d_solver.mkTerm(GT, d_solver.mkTerm(ADD, y, z), zero),
                       d_solver.mkTerm(LT, z, zero));
-  Term output;
-  d_solver.getInterpolant(conj, output);
-  Term output2;
-  d_solver.getInterpolantNext(output2);
+  Term output = d_solver.getInterpolant(conj);
+  Term output2 = d_solver.getInterpolantNext();
 
   // We expect the next output to be distinct
   ASSERT_TRUE(output != output2);
@@ -3134,9 +3127,8 @@ TEST_F(TestApiBlackSolver, proj_issue436)
     t23 = slv.mkBitVector(bw, 1);
   }
   Term t33 = slv.mkTerm(Kind::BITVECTOR_ULT, {t17, t23});
-  Term abduct;
   // solve-bv-as-int is incompatible with get-abduct
-  ASSERT_THROW(slv.getAbduct(t33, abduct), CVC5ApiException);
+  ASSERT_THROW(slv.getAbduct(t33), CVC5ApiException);
 }
   
 TEST_F(TestApiBlackSolver, proj_issue431)
@@ -3250,7 +3242,7 @@ TEST_F(TestApiBlackSolver, projIssue431)
   Term t488 = slv.mkTerm(Kind::APPLY_UF, {t31, t274});
   slv.assertFormula({t488});
   Term abduct;
-  slv.getAbduct(t488, abduct);
+  abduct = slv.getAbduct(t488);
 }
 
 }  // namespace test
diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 6bcd38e92..f4b3f7f91 100644
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -1333,7 +1333,7 @@ class SolverTest
     Term conj = d_solver.mkTerm(GT, y, zero);
     Term output = d_solver.getNullTerm();
     // Call the abduction api, while the resulting abduct is the output
-    assertTrue(d_solver.getAbduct(conj, output));
+    output = d_solver.getAbduct(conj);
     // We expect the resulting output to be a boolean formula
     assertTrue(!output.isNull() && output.getSort().isBoolean());
 
@@ -1346,7 +1346,7 @@ class SolverTest
     Term conj2 = d_solver.mkTerm(GT, x, zero);
     assertDoesNotThrow(() -> g.addRule(start, truen));
     // Call the abduction api, while the resulting abduct is the output
-    assertTrue(d_solver.getAbduct(conj2, g, output2));
+    output2 = d_solver.getAbduct(conj2, g);
     // abduct must be true
     assertEquals(output2, truen);
   }
@@ -1365,8 +1365,7 @@ class SolverTest
     Term conj = d_solver.mkTerm(GT, y, zero);
     Term output  = d_solver.getNullTerm();
     // Fails due to option not set
-    assertThrows(
-        CVC5ApiException.class, () -> d_solver.getAbduct(conj, output));
+    assertThrows(CVC5ApiException.class, () -> d_solver.getAbduct(conj));
   }
 
   @Test void getAbductNext() throws CVC5ApiException
@@ -1384,11 +1383,9 @@ class SolverTest
     d_solver.assertFormula(d_solver.mkTerm(GT, x, zero));
     // Conjecture for abduction: y > 0
     Term conj = d_solver.mkTerm(GT, y, zero);
-    Term output = d_solver.getNullTerm();
     // Call the abduction api, while the resulting abduct is the output
-    assertTrue(d_solver.getAbduct(conj, output));
-    Term output2 = d_solver.getNullTerm();
-    assertTrue(d_solver.getAbductNext(output2));
+    Term output = d_solver.getAbduct(conj);
+    Term output2 = d_solver.getAbductNext();
     // should produce a different output
     assertNotEquals(output, output2);
   }
@@ -1412,9 +1409,8 @@ class SolverTest
     // Conjecture for interpolation: y + z > 0 \/ z < 0
     Term conj = d_solver.mkTerm(
         OR, d_solver.mkTerm(GT, d_solver.mkTerm(ADD, y, z), zero), d_solver.mkTerm(LT, z, zero));
-    Term output = d_solver.getNullTerm();
     // Call the interpolation api, while the resulting interpolant is the output
-    d_solver.getInterpolant(conj, output);
+    Term output = d_solver.getInterpolant(conj);
 
     // We expect the resulting output to be a boolean formula
     assertTrue(output.getSort().isBoolean());
@@ -1436,10 +1432,8 @@ class SolverTest
     d_solver.assertFormula(d_solver.mkTerm(LT, x, zero));
     Term conj = d_solver.mkTerm(
         OR, d_solver.mkTerm(GT, d_solver.mkTerm(ADD, y, z), zero), d_solver.mkTerm(LT, z, zero));
-    Term output = d_solver.getNullTerm();
-    d_solver.getInterpolant(conj, output);
-    Term output2 = d_solver.getNullTerm();
-    d_solver.getInterpolantNext(output2);
+    Term output = d_solver.getInterpolant(conj);
+    Term output2 = d_solver.getInterpolantNext();
 
     // We expect the next output to be distinct
     assertNotEquals(output, output2);
diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index 69b08e092..a535c2502 100644
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -2078,8 +2078,7 @@ def test_get_abduct(solver):
 
     solver.assertFormula(solver.mkTerm(Kind.Gt, x, zero))
     conj = solver.mkTerm(Kind.Gt, y, zero)
-    output = cvc5.Term(solver)
-    assert solver.getAbduct(conj, output)
+    output = solver.getAbduct(conj)
     assert not output.isNull() and output.getSort().isBoolean()
 
     boolean = solver.getBooleanSort()
@@ -2089,7 +2088,7 @@ def test_get_abduct(solver):
     g = solver.mkSygusGrammar([], [start])
     conj2 = solver.mkTerm(Kind.Gt, x, zero)
     g.addRule(start, truen)
-    assert solver.getAbduct(conj2, g, output2)
+    output2 = solver.getAbduct(conj2, g)
     assert output2 == truen
 
 def test_get_abduct2(solver):
@@ -2103,7 +2102,7 @@ def test_get_abduct2(solver):
     conj = solver.mkTerm(Kind.Gt, y, zero)
     output = cvc5.Term(solver)
     with pytest.raises(RuntimeError):
-        solver.getAbduct(conj, output)
+        solver.getAbduct(conj)
 
 def test_get_abduct_next(solver):
     solver.setLogic("QF_LIA")
@@ -2117,10 +2116,8 @@ def test_get_abduct_next(solver):
 
     solver.assertFormula(solver.mkTerm(Kind.Gt, x, zero))
     conj = solver.mkTerm(Kind.Gt, y, zero)
-    output = cvc5.Term(solver)
-    assert solver.getAbduct(conj, output)
-    output2 = cvc5.Term(solver)
-    assert solver.getAbductNext(output2)
+    output = solver.getAbduct(conj)
+    output2 = solver.getAbductNext()
     assert output != output2
 
 
@@ -2142,8 +2139,7 @@ def test_get_interpolant(solver):
             Kind.Or,
             solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Add, y, z), zero),
             solver.mkTerm(Kind.Lt, z, zero))
-    output = cvc5.Term(solver)
-    solver.getInterpolant(conj, output)
+    output = solver.getInterpolant(conj)
     assert output.getSort().isBoolean()
 
 def test_get_interpolant_next(solver):
@@ -2164,10 +2160,8 @@ def test_get_interpolant_next(solver):
             Kind.Or,
             solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Add, y, z), zero),
             solver.mkTerm(Kind.Lt, z, zero))
-    output = cvc5.Term(solver)
-    solver.getInterpolant(conj, output)
-    output2 = cvc5.Term(solver)
-    solver.getInterpolantNext(output2)
+    output = solver.getInterpolant(conj)
+    output2 = solver.getInterpolantNext()
 
     assert output != output2