diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 12a90827696eabf211dcc439e2bf82aa42b49969..c0dbf1e9ab91614bef500563cab6be2df8f5e6d8 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -729,6 +729,13 @@ abstract class SMTLIBSolver(val context: LeonContext,
         unsupported("Unknown symbol: "+s)
       }
 
+    case (FunctionApplication(SimpleSymbol(SSymbol("ite")), Seq(cond, thenn, elze)), t) =>
+      IfExpr(
+        fromSMT(cond, BooleanType),
+        fromSMT(thenn, t),
+        fromSMT(elze, t)
+      )
+
     case (FunctionApplication(SimpleSymbol(s), args), tpe) if constructors.containsB(s) =>
       constructors.toA(s) match {
         case cct: CaseClassType =>