diff --git a/src/ast/converters/expr_inverter.cpp b/src/ast/converters/expr_inverter.cpp
index 63578487e..beb37193b 100644
--- a/src/ast/converters/expr_inverter.cpp
+++ b/src/ast/converters/expr_inverter.cpp
@@ -823,6 +823,35 @@ public:
 };
 #endif
 
+class finite_set_inverter : public iexpr_inverter {
+    finite_set_util fs;
+public:
+    finite_set_inverter(ast_manager& m): iexpr_inverter(m), fs(m) {}
+
+    bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r) override {
+        switch (f->get_decl_kind()) {
+        case OP_FINITE_SET_UNION:
+            // x union y -> fresh
+            // x := fresh, y := empty
+            if (num == 2 && uncnstr(args[0]) && uncnstr(args[1])) {
+                mk_fresh_uncnstr_var_for(f, r);
+                if (m_mc) {
+                    add_def(args[0], r);
+                    add_def(args[1], fs.mk_empty_set(args[1]->get_sort()));
+                }
+                return true;
+            }
+            return false;
+        default:
+            break;
+        }
+        return false;
+    }
+    
+    bool mk_diff(expr* t, expr_ref& r) override {
+        return false;
+    }
+};
 
 class seq_expr_inverter : public iexpr_inverter {
     seq_util seq;