address comments from review

yoni206 · Jun 6, 2024 · c45dcdb · c45dcdb
1 parent ede33cd
commit c45dcdb
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 14 deletions.
diff --git a/examples/api/cpp/uf.cpp b/examples/api/cpp/uf.cpp
@@ -17,24 +17,13 @@
 
 #include <iostream>
 
-using namespace std;
 using namespace cvc5;
 
-void prefixPrintGetValue(Solver& slv, Term t, int level = 0)
-{
-  cout << "slv.getValue(" << t << "): " << slv.getValue(t) << endl;
-
-  for (const Term& c : t)
-  {
-    prefixPrintGetValue(slv, c, level + 1);
-  }
-}
-
 int main()
 {
   TermManager tm;
   Solver slv(tm);
-  slv.setLogic(string("QF_UF"));
+  slv.setLogic("QF_UF");
 
   // Sorts
   Sort u = tm.mkUninterpretedSort("U");

diff --git a/examples/api/python/uf.py b/examples/api/python/uf.py
@@ -48,8 +48,8 @@
     assertions = tm.mkTerm(Kind.AND,
                             tm.mkTerm(Kind.EQUAL, x, f_x),
                             tm.mkTerm(Kind.EQUAL, y, f_y), 
-                            p_f_x.notTerm(),                            p_f_y 
-                            )
+                            p_f_x.notTerm(),
+                            p_f_y)
 
     slv.assertFormula(assertions)
     assert(slv.checkSat().isSat())