diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp
index c98af1945..562601d26 100644
--- a/src/smt/theory_finite_set.cpp
+++ b/src/smt/theory_finite_set.cpp
@@ -312,7 +312,7 @@ namespace smt {
      * - membership axioms
      * - assume eqs axioms
     */
-    final_check_status theory_finite_set::final_check_eh() {
+    final_check_status theory_finite_set::final_check_eh(unsigned) {
         TRACE(finite_set, tout << "final_check_eh\n";);
 
         if (activate_unasserted_clause())
diff --git a/src/smt/theory_finite_set.h b/src/smt/theory_finite_set.h
index 3cacd94a8..6f934e227 100644
--- a/src/smt/theory_finite_set.h
+++ b/src/smt/theory_finite_set.h
@@ -156,7 +156,7 @@ namespace smt {
         void new_eq_eh(theory_var v1, theory_var v2) override;
         void new_diseq_eh(theory_var v1, theory_var v2) override;
         void apply_sort_cnstr(enode *n, sort *s) override; 
-        final_check_status final_check_eh() override;
+        final_check_status final_check_eh(unsigned) override;
         bool can_propagate() override;
         void propagate() override;
         void assign_eh(bool_var v, bool is_true) override;