1 files changed, 12 insertions, 11 deletions
diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp
index 25529f1c8..b41cd9715 100644
--- a/examples/nra-translate/smt2toisat.cpp
+++ b/examples/nra-translate/smt2toisat.cpp
@@ -220,18 +220,19 @@ void translate_to_isat(const map<Expr, unsigned>& variables, const Expr& asserti
         cout << " -> ";
         translate_to_isat(variables, assertion[1]);
         cout << ")";
-        break;
-      case kind::IFF:
-        cout << "(";
-        translate_to_isat(variables, assertion[0]);
-        cout << " <-> ";
-        translate_to_isat(variables, assertion[1]);
-        cout << ")";
-        break;            
+        break;          
       case kind::EQUAL:
-        op = "=";
-        theory = true;
-	break;
+        if( assertion[0].getType().isBoolean() ){
+          cout << "(";
+          translate_to_isat(variables, assertion[0]);
+          cout << " <-> ";
+          translate_to_isat(variables, assertion[1]);
+          cout << ")";
+        }else{
+          op = "=";
+          theory = true;
+        }
+	      break;
       case kind::LT:
         op = "<";
         theory = true;