diff --git a/src/qe/nlarith_util.cpp b/src/qe/nlarith_util.cpp
index a66db0803..60ff87537 100644
--- a/src/qe/nlarith_util.cpp
+++ b/src/qe/nlarith_util.cpp
@@ -344,7 +344,7 @@ namespace nlarith {
 
         app* mk_or(expr* a, expr* b) {
             expr* args[2] = { a, b };
-            return mk_or(args);
+            return mk_or(2, args);
         }
         void display_branching(
             std::ostream& out, app* x,