From 88b8c9f89533a01c1f5b0b28ae080ed2311bf3e4 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Fri, 23 Sep 2016 13:30:51 +0200
Subject: [PATCH] Optimisation for mcsat solver

---
 src/mcsat/theory_mcsat.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/mcsat/theory_mcsat.ml b/src/mcsat/theory_mcsat.ml
index 187eac68..8ff16e8f 100644
--- a/src/mcsat/theory_mcsat.ml
+++ b/src/mcsat/theory_mcsat.ml
@@ -52,8 +52,9 @@ let rec iter_aux f = function
     f t
 
 let iter_assignable f = function
-  | { Expr_smt.atom = Expr_smt.Pred p } ->
-    iter_aux f p;
+  | { 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) } } ->
+    List.iter (iter_aux f) l;
   | { Expr_smt.atom = Expr_smt.Equal (a, b) } ->
     iter_aux f a; iter_aux f b