diff --git a/cozy/invariant_preservation.py b/cozy/invariant_preservation.py
index 738e8a6a..892839e2 100644
--- a/cozy/invariant_preservation.py
+++ b/cozy/invariant_preservation.py
@@ -54,6 +54,16 @@ def check_the_wf(spec : Spec):
                 res.append("at {}: `the` is illegal since its argument may not be singleton".format(pprint(e)))
     return res
 
+def check_minmax_wf(spec : Spec):
+    res = []
+    for ctx in enumerate_fragments(spec):
+        e = ctx.e
+        if isinstance(e, EArgMin) or isinstance(e, EArgMax):
+            a = ctx.facts
+            if not valid(EImplies(EAll(a), EUnaryOp(UOp.Exists, e.e).with_type(BOOL))):
+                res.append("at {}: result is ambiguous since {} could be empty".format(pprint(e), pprint(e.e)))
+    return res
+
 def check_calls_wf(spec : Spec):
     res = []
     queries = { m.name : m for m in spec.methods if isinstance(m, Query) }
diff --git a/cozy/main.py b/cozy/main.py
index d82ee449..240be13a 100755
--- a/cozy/main.py
+++ b/cozy/main.py
@@ -81,6 +81,7 @@ def run():
         errors = (
             invariant_preservation.check_ops_preserve_invariants(ast) +
             invariant_preservation.check_the_wf(ast) +
+            invariant_preservation.check_minmax_wf(ast) +
             call_errors)
         if errors:
             for e in errors: