diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc
index 2d5e93730..ee52dd518 100644
--- a/src/api/MainSolver.cc
+++ b/src/api/MainSolver.cc
@@ -337,7 +337,7 @@ sstat MainSolver::check() {
     sstat rval;
     try {
         rval = simplifyFormulas();
-    } catch (opensmt::NonLinException const & error) {
+    } catch (NonLinException const & error) {
         reasonUnknown = error.what();
         return s_Undef;
     }
@@ -347,7 +347,7 @@ sstat MainSolver::check() {
     if (rval == s_Undef) {
         try {
             rval = solve();
-        } catch (std::overflow_error const & error) { rval = s_Error; } catch (opensmt::NonLinException const & error) {
+        } catch (std::overflow_error const & error) { rval = s_Error; } catch (NonLinException const & error) {
             reasonUnknown = error.what();
             return s_Undef;
         }
diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc
index 5f2079d2b..5f68a2489 100644
--- a/src/logics/ArithLogic.cc
+++ b/src/logics/ArithLogic.cc
@@ -2,6 +2,7 @@
 
 #include <common/ApiException.h>
 #include <common/InternalException.h>
+#include <common/NonLinException.h>
 #include <common/StringConv.h>
 #include <common/TreeOps.h>
 #include <pterms/PtStore.h>
@@ -863,7 +864,9 @@ PTRef ArithLogic::mkRealDiv(vec<PTRef> && args) {
     vec<PTRef> args_new;
     SymRef s_new;
     simp.simplify(get_sym_Real_DIV(), args, s_new, args_new);
-    if (isRealDiv(s_new) && (isNumTerm(args_new[0]) || isPlus(args_new[0])) && isConstant(args_new[1])) {
+    // TODO: Currently creation of nonlinear Real divison is not supported
+    if (isRealDiv(s_new) && (isNumTerm(args_new[0]) || isPlus(args_new[0]))) {
+        if (!isConstant(args_new[1])) throw NonLinException(pp(args[0]) + "/" + pp(args[1]));
         args_new[1] = mkRealConst(getNumConst(args_new[1]).inverse()); // mkConst(1/getRealConst(args_new[1]));
         return mkTimes(args_new);
     }
diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc
index b89a726fb..5f23e93e6 100644
--- a/src/tsolvers/lasolver/LASolver.cc
+++ b/src/tsolvers/lasolver/LASolver.cc
@@ -92,7 +92,7 @@ void LASolver::isProperLeq(PTRef tr)
     assert(logic.isLeq(tr));
     auto [cons, sum] = logic.leqToConstantAndTerm(tr);
     assert(logic.isConstant(cons));
-    assert(logic.isNumVar(sum) || logic.isPlus(sum) || logic.isTimesLinOrNonlin(sum) || logic.isRealDiv(sum));
+    assert(logic.isNumVar(sum) || logic.isPlus(sum) || logic.isTimesLinOrNonlin(sum));
     (void) cons; (void)sum;
 }
 
@@ -243,7 +243,7 @@ LVRef LASolver::getVarForLeq(PTRef ref) const {
 }
 
 LVRef LASolver::getLAVar_single(PTRef expr_in) {
-    if (logic.isTimesNonlin(expr_in) || logic.isRealDiv(expr_in)) throw NonLinException(logic.pp(expr_in));
+    if (logic.isTimesNonlin(expr_in)) throw NonLinException(logic.pp(expr_in));
     assert(logic.isLinearTerm(expr_in));
     PTId id = logic.getPterm(expr_in).getId();
 
diff --git a/test/regression/base/arithmetic/miniexample1.smt2 b/test/regression/base/arithmetic/miniexample1.smt2
index 15bd69389..6915ae214 100644
--- a/test/regression/base/arithmetic/miniexample1.smt2
+++ b/test/regression/base/arithmetic/miniexample1.smt2
@@ -1,5 +1,5 @@
 (set-logic QF_LRA)
-(define-fun uninterp_div ((a Real) (b Real)) Real (/ a b))
-(assert (= (uninterp_div 1 2) 0.5))
+(define-fun uninterp_div ((a Real) (b Real)) Real (* a b))
+(assert (= (uninterp_div 0.25 2) 0.5))
 (check-sat)
 (exit)
diff --git a/test/regression/base/arithmetic/miniexample4.smt2 b/test/regression/base/arithmetic/miniexample4.smt2
deleted file mode 100644
index 4f6320543..000000000
--- a/test/regression/base/arithmetic/miniexample4.smt2
+++ /dev/null
@@ -1,7 +0,0 @@
-(set-logic QF_LRA)
-(declare-fun x () Real)
-(declare-fun y () Real)
-(define-fun uninterp_div ((a Real) (b Real)) Real (/ a b))
-(assert (= (uninterp_div y x) 20))
-(check-sat)
-(exit)
diff --git a/test/regression/base/arithmetic/miniexample4.smt2.expected.err b/test/regression/base/arithmetic/miniexample4.smt2.expected.err
deleted file mode 100644
index e69de29bb..000000000
diff --git a/test/regression/base/arithmetic/miniexample4.smt2.expected.out b/test/regression/base/arithmetic/miniexample4.smt2.expected.out
deleted file mode 100644
index 354664565..000000000
--- a/test/regression/base/arithmetic/miniexample4.smt2.expected.out
+++ /dev/null
@@ -1 +0,0 @@
-unknown
diff --git a/test/regression/base/arithmetic/miniexample4_Ok.smt2 b/test/regression/base/arithmetic/miniexample4_Ok.smt2
deleted file mode 100644
index 83b26639b..000000000
--- a/test/regression/base/arithmetic/miniexample4_Ok.smt2
+++ /dev/null
@@ -1,8 +0,0 @@
-(set-logic QF_LRA)
-(declare-fun x () Real)
-(declare-fun y () Real)
-(define-fun uninterp_div ((a Real) (b Real)) Real (/ a b))
-(assert (= (uninterp_div y 5) (+ 3 x)))
-(check-sat)
-(get-model)
-(exit)
diff --git a/test/regression/base/arithmetic/miniexample4_Ok.smt2.expected.err b/test/regression/base/arithmetic/miniexample4_Ok.smt2.expected.err
deleted file mode 100644
index e69de29bb..000000000
diff --git a/test/regression/base/arithmetic/miniexample4_Ok.smt2.expected.out b/test/regression/base/arithmetic/miniexample4_Ok.smt2.expected.out
deleted file mode 100644
index e009558ce..000000000
--- a/test/regression/base/arithmetic/miniexample4_Ok.smt2.expected.out
+++ /dev/null
@@ -1,7 +0,0 @@
-sat
-(
-  (define-fun x () Real
-    0)
-  (define-fun y () Real
-    15)
-)