diff --git a/src/solver/solver.h b/src/solver/solver.h
index 5329161cd..7437a5a08 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -146,6 +146,8 @@ public:
     
     lbool check_sat(app_ref_vector const& asms) { return check_sat(asms.size(), (expr* const*)asms.c_ptr()); }
 
+    lbool check_sat() { return check_sat(0, nullptr); }
+
     /**
        \brief Check satisfiability modulo a cube and a clause.
 
diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp
index 4ba3b3b5c..9ab3123a2 100644
--- a/src/util/gparams.cpp
+++ b/src/util/gparams.cpp
@@ -520,7 +520,7 @@ public:
             try {
                 symbol m, p;
                 normalize(name, m, p);
-                std::cout << name << " " << m << " " << p << "\n";
+                out << name << " " << m << " " << p << "\n";
                 param_descrs * d;
                 if (m == symbol::null) {
                     d = &get_param_descrs();