diff --git a/src/mcsat/theory_mcsat.ml b/src/mcsat/theory_mcsat.ml
index 46b718ae..cc0afcf3 100644
--- a/src/mcsat/theory_mcsat.ml
+++ b/src/mcsat/theory_mcsat.ml
@@ -128,7 +128,8 @@ let rec iter_aux f = function
 
 let iter_assignable f = function
   | { Expr_smt.atom = Expr_smt.Pred { Expr_smt.term = Expr_smt.Var _ } } -> ()
-  | { Expr_smt.atom = Expr_smt.Pred { Expr_smt.term = Expr_smt.App (_, _, l) } } ->
+  | { Expr_smt.atom = Expr_smt.Pred ({ Expr_smt.term = Expr_smt.App (_, _, l) } as t) } ->
+    if l <> [] then add_watch t (t :: l);
     List.iter (iter_aux f) l;
   | { Expr_smt.atom = Expr_smt.Equal (a, b) } ->
     iter_aux f a; iter_aux f b
diff --git a/tests/unsat/test-013.smt2 b/tests/unsat/test-013.smt2
new file mode 100644
index 00000000..d67c8f07
--- /dev/null
+++ b/tests/unsat/test-013.smt2
@@ -0,0 +1,2 @@
+(assert (and (= a b) (not (p a)) (p b)))
+(check-sat)