From eb205a5a4005d5267cfe39a4acdf3b96a6943ef5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 15 Feb 2020 21:26:02 -1000
Subject: [PATCH] fix #3011

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/nlsat/tactic/goal2nlsat.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/nlsat/tactic/goal2nlsat.cpp b/src/nlsat/tactic/goal2nlsat.cpp
index 04f7f9d06..4c4483d1f 100644
--- a/src/nlsat/tactic/goal2nlsat.cpp
+++ b/src/nlsat/tactic/goal2nlsat.cpp
@@ -201,6 +201,7 @@ struct goal2nlsat::imp {
                 case OP_XOR:
                 case OP_NOT:
                 case OP_IMPLIES:
+                case OP_ITE:
                     throw tactic_exception("convert goal into cnf before applying nlsat");
                 case OP_DISTINCT:
                     throw tactic_exception("eliminate distinct operator (use tactic '(using-params simplify :blast-distinct true)') before applying nlsat");