1 files changed, 11 insertions, 4 deletions
diff --git a/examples/api/sygus-inv.cpp b/examples/api/sygus-inv.cpp
index 820fe8630..f658fa33a 100644
--- a/examples/api/sygus-inv.cpp
+++ b/examples/api/sygus-inv.cpp
@@ -30,14 +30,18 @@
  *
  * (check-synth)
  *
- * The printed output to this example should be equivalent to:
- * (define-fun inv-f ((x Int)) Bool (not (>= x 11)))
+ * The printed output for this example should be equivalent to:
+ * (
+ *   (define-fun inv-f ((x Int)) Bool (not (>= x 11)))
+ * )
  */
 
 #include <cvc5/cvc5.h>
 
 #include <iostream>
 
+#include "utils.h"
+
 using namespace cvc5::api;
 
 int main()
@@ -82,8 +86,11 @@ int main()
   if (slv.checkSynth().isUnsat())
   {
     // Output should be equivalent to:
-    // (define-fun inv-f ((x Int)) Bool (not (>= x 11)))
-    slv.printSynthSolution(std::cout);
+    // (
+    //   (define-fun inv-f ((x Int)) Bool (not (>= x 11)))
+    // )
+    std::vector<Term> terms = {inv_f};
+    printSynthSolutions(terms, slv.getSynthSolutions(terms));
   }
 
   return 0;