diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc
index 44b6bb28b..ee52dd518 100644
--- a/src/api/MainSolver.cc
+++ b/src/api/MainSolver.cc
@@ -9,6 +9,7 @@
 #include "MainSolver.h"
 
 #include <common/ApiException.h>
+#include <common/NonLinException.h>
 #include <itehandler/IteHandler.h>
 #include <logics/ArrayTheory.h>
 #include <logics/LATheory.h>
@@ -333,14 +334,23 @@ sstat MainSolver::check() {
         StopWatch sw(query_timer);
     }
     if (isLastFrameUnsat()) { return s_False; }
-    sstat rval = simplifyFormulas();
+    sstat rval;
+    try {
+        rval = simplifyFormulas();
+    } catch (NonLinException const & error) {
+        reasonUnknown = error.what();
+        return s_Undef;
+    }
 
     if (config.dump_query()) printCurrentAssertionsAsQuery();
 
     if (rval == s_Undef) {
         try {
             rval = solve();
-        } catch (std::overflow_error const & error) { rval = s_Error; }
+        } catch (std::overflow_error const & error) { rval = s_Error; } catch (NonLinException const & error) {
+            reasonUnknown = error.what();
+            return s_Undef;
+        }
         if (rval == s_False) {
             assert(not smt_solver->isOK());
             rememberUnsatFrame(smt_solver->getConflictFrame());
diff --git a/src/api/MainSolver.h b/src/api/MainSolver.h
index 01fc6ad37..ae94117b2 100644
--- a/src/api/MainSolver.h
+++ b/src/api/MainSolver.h
@@ -258,7 +258,7 @@ class MainSolver {
     PTRef newFrameTerm(FrameId frameId) {
         assert(frameId != 0);
         auto name = std::string(Logic::s_framev_prefix) + std::to_string(frameId);
-        PTRef frameTerm = logic.mkBoolVar(name.c_str());
+        PTRef frameTerm = logic.mkInternalBoolVar(name.c_str());
         Lit l = term_mapper->getOrCreateLit(frameTerm);
         term_mapper->setFrozen(var(l));
         smt_solver->addAssumptionVar(var(l));
@@ -310,6 +310,7 @@ class MainSolver {
     vec<PTRef> frameTerms;
     std::size_t firstNotSimplifiedFrame = 0;
     unsigned int insertedFormulasCount = 0;
+    std::string reasonUnknown;
 };
 
 bool MainSolver::trackPartitions() const {
diff --git a/src/common/CMakeLists.txt b/src/common/CMakeLists.txt
index ed6e244aa..fcb542f1a 100644
--- a/src/common/CMakeLists.txt
+++ b/src/common/CMakeLists.txt
@@ -24,5 +24,5 @@ include(numbers/CMakeLists.txt)
 install(FILES
         StringMap.h Timer.h inttypes.h IColor.h
         TreeOps.h FlaPartitionMap.h PartitionInfo.h Partitions.h ApiException.h TypeUtils.h
-        NatSet.h ScopedVector.h TermNames.h
+        NatSet.h ScopedVector.h TermNames.h NonLinException.h
 DESTINATION ${INSTALL_HEADERS_DIR}/common)
diff --git a/src/common/NonLinException.h b/src/common/NonLinException.h
new file mode 100644
index 000000000..6962bfbb8
--- /dev/null
+++ b/src/common/NonLinException.h
@@ -0,0 +1,19 @@
+/*
+*  Copyright (c) 2024, Konstantin Britikov <britikovki@gmail.com>
+*
+*  SPDX-License-Identifier: MIT
+*/
+
+#ifndef OPENSMT_NONLINEXCEPTION_H
+#define OPENSMT_NONLINEXCEPTION_H
+
+#include <stdexcept>
+
+namespace opensmt {
+class NonLinException : public std::runtime_error {
+public:
+    NonLinException(std::string_view const reason_) : runtime_error("Term " + std::string(reason_) + " is non-linear"){}
+};
+}
+
+#endif // OPENSMT_NONLINEXCEPTION_H
diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc
index 74c8b86c7..871121cbb 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>
@@ -114,6 +115,8 @@ ArithLogic::ArithLogic(Logic_t type)
       sym_Real_MINUS(declareFun_NoScoping_LeftAssoc(tk_real_minus, sort_REAL, {sort_REAL, sort_REAL})),
       sym_Real_PLUS(declareFun_Commutative_NoScoping_LeftAssoc(tk_real_plus, sort_REAL, {sort_REAL, sort_REAL})),
       sym_Real_TIMES(declareFun_Commutative_NoScoping_LeftAssoc(tk_real_times, sort_REAL, {sort_REAL, sort_REAL})),
+      sym_Real_TIMES_LIN(declareFunMultiplicationLinNonlin(tk_real_times, sort_REAL, {sort_REAL, sort_REAL})),
+      sym_Real_TIMES_NONLIN(declareFunMultiplicationLinNonlin(tk_real_times, sort_REAL, {sort_REAL, sort_REAL})),
       sym_Real_DIV(declareFun_NoScoping_LeftAssoc(tk_real_div, sort_REAL, {sort_REAL, sort_REAL})),
       sym_Real_EQ(sortToEquality[sort_REAL]),
       sym_Real_LEQ(declareFun_NoScoping_Chainable(tk_real_leq, sort_BOOL, {sort_REAL, sort_REAL})),
@@ -134,6 +137,8 @@ ArithLogic::ArithLogic(Logic_t type)
       sym_Int_MINUS(declareFun_NoScoping_LeftAssoc(tk_int_minus, sort_INT, {sort_INT, sort_INT})),
       sym_Int_PLUS(declareFun_Commutative_NoScoping_LeftAssoc(tk_int_plus, sort_INT, {sort_INT, sort_INT})),
       sym_Int_TIMES(declareFun_Commutative_NoScoping_LeftAssoc(tk_int_times, sort_INT, {sort_INT, sort_INT})),
+      sym_Int_TIMES_LIN(declareFunMultiplicationLinNonlin(tk_int_times, sort_INT, {sort_INT, sort_INT})),
+      sym_Int_TIMES_NONLIN(declareFunMultiplicationLinNonlin(tk_int_times, sort_INT, {sort_INT, sort_INT})),
       sym_Int_DIV(declareFun_NoScoping_LeftAssoc(tk_int_div, sort_INT, {sort_INT, sort_INT})),
       sym_Int_MOD(declareFun_NoScoping(tk_int_mod, sort_INT, {sort_INT, sort_INT})),
       sym_Int_EQ(sortToEquality[sort_INT]),
@@ -149,9 +154,14 @@ SymRef ArithLogic::getPlusForSort(SRef sort) const {
     return sort == getSort_int() ? get_sym_Int_PLUS() : get_sym_Real_PLUS();
 }
 
-SymRef ArithLogic::getTimesForSort(SRef sort) const {
+SymRef ArithLogic::getTimesLinForSort(SRef sort) const {
     assert(sort == getSort_int() or sort == getSort_real());
-    return sort == getSort_int() ? get_sym_Int_TIMES() : get_sym_Real_TIMES();
+    return sort == getSort_int() ? get_sym_Int_TIMES_LIN() : get_sym_Real_TIMES_LIN();
+}
+
+SymRef ArithLogic::getTimesNonlinForSort(SRef sort) const {
+    assert(sort == getSort_int() or sort == getSort_real());
+    return sort == getSort_int() ? get_sym_Int_TIMES_NONLIN() : get_sym_Real_TIMES_NONLIN();
 }
 
 SymRef ArithLogic::getMinusForSort(SRef sort) const {
@@ -175,11 +185,11 @@ PTRef ArithLogic::getMinusOneForSort(SRef sort) const {
 }
 
 bool ArithLogic::isLinearFactor(PTRef tr) const {
-    if (isNumConst(tr) || isNumVarLike(tr)) { return true; }
-    if (isTimes(tr)) {
+    if (isNumConst(tr) || isMonomial(tr)) { return true; }
+    if (isTimesLin(tr)) {
         Pterm const & term = getPterm(tr);
         return term.size() == 2 &&
-               ((isNumConst(term[0]) && (isNumVarLike(term[1]))) || (isNumConst(term[1]) && (isNumVarLike(term[0]))));
+               ((isNumConst(term[0]) && (isMonomial(term[1]))) || (isNumConst(term[1]) && (isMonomial(term[0]))));
     }
     return false;
 }
@@ -209,7 +219,6 @@ pair<Number, vec<PTRef>> ArithLogic::getConstantAndFactors(PTRef sum) const {
             assert(constant == PTRef_Undef);
             constant = arg;
         } else {
-            assert(isLinearFactor(arg));
             varFactors.push(arg);
         }
     }
@@ -220,17 +229,17 @@ pair<Number, vec<PTRef>> ArithLogic::getConstantAndFactors(PTRef sum) const {
     return {std::move(constantValue), std::move(varFactors)};
 }
 
-pair<PTRef, PTRef> ArithLogic::splitTermToVarAndConst(PTRef term) const {
-    assert(isTimes(term) || isNumVarLike(term) || isConstant(term));
-    if (isTimes(term)) {
+pair<PTRef, PTRef> ArithLogic::splitPolyTerm(PTRef term) const {
+    assert(isTimes(term) || isMonomial(term) || isConstant(term));
+    if (isTimesLin(term)) {
         assert(getPterm(term).size() == 2);
         PTRef fac = getPterm(term)[0];
         PTRef var = getPterm(term)[1];
         if (not isConstant(fac)) { std::swap(fac, var); }
         assert(isConstant(fac));
-        assert(isNumVarLike(var));
+        assert(isMonomial(var));
         return {var, fac};
-    } else if (isNumVarLike(term)) {
+    } else if (isMonomial(term)) {
         assert(yieldsSortInt(term) or yieldsSortReal(term));
         PTRef var = term;
         PTRef fac = yieldsSortInt(term) ? getTerm_IntOne() : getTerm_RealOne();
@@ -243,8 +252,8 @@ pair<PTRef, PTRef> ArithLogic::splitTermToVarAndConst(PTRef term) const {
 
 // Normalize a product of the form (* a v) to either v or (* -1 v)
 PTRef ArithLogic::normalizeMul(PTRef mul) {
-    assert(isTimes(mul));
-    auto [v, c] = splitTermToVarAndConst(mul);
+    assert(isTimesLinOrNonlin(mul));
+    auto [v, c] = splitPolyTerm(mul);
     if (getNumConst(c) < 0) {
         return mkNeg(v);
     } else {
@@ -401,15 +410,14 @@ lbool ArithLogic::arithmeticElimination(vec<PTRef> const & top_level_arith, Subs
         PTRef lhs = logic.getPterm(eq)[0];
         PTRef rhs = logic.getPterm(eq)[1];
         PTRef polyTerm = lhs == logic.getZeroForSort(logic.getSortRef(lhs)) ? rhs : logic.mkMinus(rhs, lhs);
-        assert(logic.isLinearTerm(polyTerm));
         if (logic.isLinearFactor(polyTerm)) {
-            auto [var, c] = logic.splitTermToVarAndConst(polyTerm);
+            auto [var, c] = logic.splitPolyTerm(polyTerm);
             auto coeff = logic.getNumConst(c);
             poly.addTerm(var, std::move(coeff));
         } else {
-            assert(logic.isPlus(polyTerm));
+            assert(logic.isPlus(polyTerm) || logic.isTimesNonlin(polyTerm));
             for (PTRef factor : logic.getPterm(polyTerm)) {
-                auto [var, c] = logic.splitTermToVarAndConst(factor);
+                auto [var, c] = logic.splitPolyTerm(factor);
                 auto coeff = logic.getNumConst(c);
                 poly.addTerm(var, std::move(coeff));
             }
@@ -476,14 +484,14 @@ pair<lbool, Logic::SubstMap> ArithLogic::retrieveSubstitutions(vec<PtAsgn> const
 }
 
 uint32_t LessThan_deepPTRef::getVarIdFromProduct(PTRef tr) const {
-    assert(l.isTimes(tr));
-    auto [v, c] = l.splitTermToVarAndConst(tr);
+    assert(l.isTimesLinOrNonlin(tr));
+    auto [v, c] = l.splitPolyTerm(tr);
     return v.x;
 }
 
 bool LessThan_deepPTRef::operator()(PTRef x_, PTRef y_) const {
-    uint32_t id_x = l.isTimes(x_) ? getVarIdFromProduct(x_) : x_.x;
-    uint32_t id_y = l.isTimes(y_) ? getVarIdFromProduct(y_) : y_.x;
+    uint32_t id_x = l.isTimesLinOrNonlin(x_) ? getVarIdFromProduct(x_) : x_.x;
+    uint32_t id_y = l.isTimesLinOrNonlin(y_) ? getVarIdFromProduct(y_) : y_.x;
     return id_x < id_y;
 }
 
@@ -498,10 +506,10 @@ bool ArithLogic::isBuiltinFunction(SymRef const sr) const {
         return Logic::isBuiltinFunction(sr);
 }
 bool ArithLogic::isNumTerm(PTRef tr) const {
-    if (isNumVarLike(tr)) return true;
+    if (isMonomial(tr)) return true;
     Pterm const & t = getPterm(tr);
-    if (t.size() == 2 && isTimes(tr))
-        return (isNumVarLike(t[0]) && isConstant(t[1])) || (isNumVarLike(t[1]) && isConstant(t[0]));
+    if (t.size() == 2 && isTimesLin(tr))
+        return (isMonomial(t[0]) && isConstant(t[1])) || (isMonomial(t[1]) && isConstant(t[0]));
     else if (t.size() == 0)
         return isNumVar(tr) || isConstant(tr);
     else
@@ -511,11 +519,11 @@ bool ArithLogic::isNumTerm(PTRef tr) const {
 PTRef ArithLogic::mkNeg(PTRef tr) {
     assert(!isNeg(tr)); // MB: The invariant now is that there is no "Minus" node
     SymRef symref = getSymRef(tr);
-    if (isConstant(symref)) {
+    if (isConstant(tr)) {
         Number const & v = getNumConst(tr);
         return mkConst(getSortRef(tr), -v);
     }
-    if (isPlus(symref)) {
+    if (isPlus(tr)) {
         vec<PTRef> args;
         args.capacity(getPterm(tr).size());
         // Note: Do this in two phases to avoid calling mkNeg that invalidates the Pterm reference
@@ -529,14 +537,14 @@ PTRef ArithLogic::mkNeg(PTRef tr) {
         PTRef tr_n = mkFun(symref, std::move(args));
         return tr_n;
     }
-    if (isTimes(symref)) { // constant * var-like
+    if (isTimesLin(tr)) { // constant * monomial
         assert(getPterm(tr).size() == 2);
-        auto [var, constant] = splitTermToVarAndConst(tr);
+        auto [var, constant] = splitPolyTerm(tr);
         return constant == getMinusOneForSort(getSortRef(symref)) ? var : mkFun(symref, {var, mkNeg(constant)});
     }
-    if (isNumVarLike(symref)) {
+    if (isMonomial(tr)) {
         auto sortRef = getSortRef(symref);
-        return mkFun(getTimesForSort(sortRef), {tr, getMinusOneForSort(sortRef)});
+        return mkFun(getTimesLinForSort(sortRef), {tr, getMinusOneForSort(sortRef)});
     }
     // MB: All cases should be covered
     throw InternalException("Failed attempt to negate a term");
@@ -604,7 +612,7 @@ PTRef ArithLogic::mkPlus(vec<PTRef> && args) {
     simplified.reserve(args.size());
 
     for (PTRef arg : args) {
-        auto [v, c] = splitTermToVarAndConst(arg);
+        auto [v, c] = splitPolyTerm(arg);
         assert(c != PTRef_Undef);
         assert(isConstant(c));
         if (not varIndices.has(v)) {
@@ -635,7 +643,7 @@ PTRef ArithLogic::mkPlus(vec<PTRef> && args) {
             continue;
         }
         // default case, variable and constant (cannot be simplified)
-        PTRef term = mkFun(getTimesForSort(returnSort), {coeffTerm, var});
+        PTRef term = mkFun(getTimesLinForSort(returnSort), {coeffTerm, var});
         flattened_args.push(term);
     }
     if (flattened_args.size() == 0) return getZeroForSort(returnSort);
@@ -669,15 +677,28 @@ PTRef ArithLogic::mkTimes(vec<PTRef> && args) {
     SimplifyConstTimes simp(*this);
     args.clear();
     SymRef s_new;
-    simp.simplify(getTimesForSort(returnSort), flatten_args, s_new, args);
-    PTRef tr = mkFun(s_new, std::move(args));
-    // Either a real term or, if we constructed a multiplication of a
-    // constant and a sum, a real sum.
-    if (isNumTerm(tr) || isPlus(tr) || isUF(tr) || isIte(tr))
-        return tr;
-    else {
-        auto termStr = pp(tr);
-        throw LANonLinearException(termStr.c_str());
+    simp.simplify(getTimesLinForSort(returnSort), flatten_args, s_new, args);
+    if (!isTimesLinOrNonlin(s_new)) return mkFun(s_new, std::move(args));
+    PTRef coef = PTRef_Undef;
+    std::vector<PTRef> vars;
+    // Splitting Multiplication into constant and monomial subterms
+    for (int i = 0; i < args.size(); i++) {
+        if (isConstant(args[i])) {
+            assert(coef == PTRef_Undef);
+            coef = args[i];
+            continue;
+        }
+        vars.push_back(args[i]);
+    }
+    assert(!vars.empty());
+    if (vars.size() > 1) {
+        if (coef == PTRef_Undef) {
+            return mkFun(getTimesNonlinForSort(returnSort), vars);
+        } else {
+            return mkFun(s_new, {coef, mkFun(getTimesNonlinForSort(returnSort), vars)});
+        }
+    } else {
+        return mkFun(s_new, {coef, vars[0]});
     }
 }
 
@@ -705,9 +726,9 @@ PTRef ArithLogic::mkBinaryLeq(PTRef lhs, PTRef rhs) {
         Number const & v = this->getNumConst(sum_tmp);
         return v.sign() < 0 ? getTerm_false() : getTerm_true();
     }
-    if (isNumVarLike(sum_tmp) ||
-        isTimes(sum_tmp)) { // "sum_tmp = c * v", just scale to "v" or "-v" without changing the sign
-        sum_tmp = isTimes(sum_tmp) ? normalizeMul(sum_tmp) : sum_tmp;
+    if (isMonomial(sum_tmp) ||
+        isTimesLinOrNonlin(sum_tmp)) { // "sum_tmp = c * v", just scale to "v" or "-v" without changing the sign
+        sum_tmp = isTimesLinOrNonlin(sum_tmp) ? normalizeMul(sum_tmp) : sum_tmp;
         return mkFun(getLeqForSort(argSort), {getZeroForSort(argSort), sum_tmp});
     } else if (isPlus(sum_tmp)) {
         // Normalize the sum
@@ -778,8 +799,8 @@ PTRef ArithLogic::mkBinaryEq(PTRef lhs, PTRef rhs) {
     if (isConstant(diff)) {
         Number const & v = this->getNumConst(diff);
         return v.isZero() ? getTerm_true() : getTerm_false();
-    } else if (isNumVarLike(diff) || isTimes(diff)) {
-        auto [var, constant] = splitTermToVarAndConst(diff);
+    } else if (isMonomial(diff) || isTimesLin(diff)) {
+        auto [var, constant] = splitPolyTerm(diff);
         return Logic::mkBinaryEq(getZeroForSort(eqSort),
                                  var); // Avoid anything that calls Logic::mkEq as this would create a loop
     } else if (isPlus(diff)) {
@@ -795,11 +816,9 @@ PTRef ArithLogic::mkMod(vec<PTRef> && args) {
     checkSortInt(args);
     PTRef dividend = args[0];
     PTRef divisor = args[1];
-
-    if (not isNumConst(divisor)) { throw ApiException("Divisor must be constant in linear logic"); }
     if (isZero(divisor)) { throw ArithDivisionByZeroException(); }
     if (isOne(divisor) or isMinusOne(divisor)) { return getTerm_IntZero(); }
-    if (isConstant(dividend)) {
+    if (isConstant(dividend) && isConstant(divisor)) {
         auto const & dividendValue = getNumConst(dividend);
         auto const & divisorValue = getNumConst(divisor);
         assert(dividendValue.isInteger() and divisorValue.isInteger());
@@ -818,7 +837,6 @@ PTRef ArithLogic::mkIntDiv(vec<PTRef> && args) {
     assert(args.size() == 2);
     PTRef dividend = args[0];
     PTRef divisor = args[1];
-    if (not isConstant(divisor)) { throw LANonLinearException("Divisor must be constant in linear logic"); }
     if (isZero(divisor)) { throw ArithDivisionByZeroException(); }
     if (isOne(divisor)) { return dividend; }
     if (isMinusOne(divisor)) { return mkNeg(dividend); }
@@ -839,13 +857,12 @@ PTRef ArithLogic::mkRealDiv(vec<PTRef> && args) {
     checkSortReal(args);
     if (args.size() != 2) { throw ApiException("Division operation requires exactly 2 arguments"); }
     if (isZero(args[1])) { throw ArithDivisionByZeroException(); }
-    if (not isConstant(args[1])) {
-        throw LANonLinearException("Only division by constant is permitted in linear arithmetic!");
-    }
+    if (not isConstant(args[1])) { throw NonLinException(pp(args[0]) + "/" + pp(args[1])); }
     SimplifyConstDiv simp(*this);
     vec<PTRef> args_new;
     SymRef s_new;
     simp.simplify(get_sym_Real_DIV(), args, s_new, args_new);
+    // TODO: Currently creation of nonlinear Real divison (with variable divisor) is not supported
     if (isRealDiv(s_new)) {
         assert((isNumTerm(args_new[0]) || isPlus(args_new[0])) && isConstant(args_new[1]));
         args_new[1] = mkRealConst(getNumConst(args_new[1]).inverse()); // mkConst(1/getRealConst(args_new[1]));
@@ -982,7 +999,7 @@ void SimplifyConst::simplify(SymRef s, vec<PTRef> const & args, SymRef & s_new,
     }
     //    // A single argument for the operator, and the operator is identity
     //    // in that case
-    if (args_new.size() == 1 && (l.isPlus(s_new) || l.isTimes(s_new))) {
+    if (args_new.size() == 1 && (l.isPlus(s_new) || l.isTimesLin(s_new))) {
         PTRef ch_tr = args_new[0];
         args_new.clear();
         s_new = l.getPterm(ch_tr).symb();
@@ -1200,8 +1217,8 @@ pair<Number, PTRef> ArithLogic::sumToNormalizedIntPair(PTRef sum) {
     std::vector<Number> coeffs;
     coeffs.reserve(varFactors.size());
     for (PTRef factor : varFactors) {
-        auto [var, coeff] = splitTermToVarAndConst(factor);
-        assert(ArithLogic::isNumVarLike(var) and isNumConst(coeff));
+        auto [var, coeff] = splitPolyTerm(factor);
+        assert(ArithLogic::isMonomial(var) and isNumConst(coeff));
         vars.push(var);
         coeffs.push_back(getNumConst(coeff));
     }
@@ -1278,7 +1295,7 @@ pair<Number, PTRef> ArithLogic::sumToNormalizedRealPair(PTRef sum) {
 
     PTRef leadingFactor = varFactors[0];
     // normalize the sum according to the leading factor
-    auto [var, coeff] = splitTermToVarAndConst(leadingFactor);
+    auto [var, coeff] = splitPolyTerm(leadingFactor);
     Number normalizationCoeff = abs(getNumConst(coeff));
     // varFactors come from a normalized sum, no need to call normalization code again
     PTRef normalizedSum = varFactors.size() == 1 ? varFactors[0] : mkFun(get_sym_Real_PLUS(), std::move(varFactors));
@@ -1340,14 +1357,14 @@ std::pair<PTRef, PTRef> ArithLogic::leqToConstantAndTerm(PTRef leq) {
 }
 
 bool ArithLogic::hasNegativeLeadingVariable(PTRef poly) const {
-    if (isNumConst(poly) or isNumVarLike(poly)) { return false; }
-    if (isTimes(poly)) {
-        auto [var, constant] = splitTermToVarAndConst(poly);
+    if (isNumConst(poly) or isMonomial(poly)) { return false; }
+    if (isTimesLinOrNonlin(poly)) {
+        auto [var, constant] = splitPolyTerm(poly);
         return isNegative(getNumConst(constant));
     }
     assert(isPlus(poly));
     PTRef leadingTerm = getPterm(poly)[0];
-    auto [var, constant] = splitTermToVarAndConst(leadingTerm);
+    auto [var, constant] = splitPolyTerm(leadingTerm);
     return isNegative(getNumConst(constant));
 }
 } // namespace opensmt
diff --git a/src/logics/ArithLogic.h b/src/logics/ArithLogic.h
index ecbdc9348..77bc11d11 100644
--- a/src/logics/ArithLogic.h
+++ b/src/logics/ArithLogic.h
@@ -8,16 +8,6 @@
 #include <numeric>
 
 namespace opensmt {
-class LANonLinearException : public std::runtime_error {
-public:
-    LANonLinearException(char const * reason_) : runtime_error(reason_) {
-        msg = "Term " + std::string(reason_) + " is non-linear";
-    }
-    virtual char const * what() const noexcept override { return msg.c_str(); }
-
-private:
-    std::string msg;
-};
 
 class ArithDivisionByZeroException : public std::runtime_error {
 public:
@@ -105,6 +95,10 @@ class ArithLogic : public Logic {
 
     SymRef get_sym_Int_TIMES() const { return sym_Int_TIMES; }
     SymRef get_sym_Real_TIMES() const { return sym_Real_TIMES; }
+    SymRef get_sym_Int_TIMES_LIN() const { return sym_Int_TIMES_LIN; }
+    SymRef get_sym_Real_TIMES_LIN() const { return sym_Real_TIMES_LIN; }
+    SymRef get_sym_Int_TIMES_NONLIN() const { return sym_Int_TIMES_NONLIN; }
+    SymRef get_sym_Real_TIMES_NONLIN() const { return sym_Real_TIMES_NONLIN; }
     SymRef get_sym_Int_DIV() const { return sym_Int_DIV; }
     SymRef get_sym_Int_MOD() const { return sym_Int_MOD; }
     SymRef get_sym_Real_DIV() const { return sym_Real_DIV; }
@@ -170,10 +164,22 @@ class ArithLogic : public Logic {
     bool isIntNeg(SymRef sr) const { return sr == sym_Int_NEG; }
     bool isRealNeg(SymRef sr) const { return sr == sym_Real_NEG; }
 
-    bool isTimes(SymRef sr) const { return isIntTimes(sr) or isRealTimes(sr); }
+    bool isTimes(SymRef sr) const { return isTimesLin(sr) or isTimesNonlin(sr) or isIntTimes(sr) or isRealTimes(sr); };
+    bool isTimesLinOrNonlin(SymRef sr) const { return isTimesLin(sr) or isTimesNonlin(sr); };
+    bool isTimesLin(SymRef sr) const { return isIntTimesLin(sr) or isRealTimesLin(sr); }
+    bool isTimesNonlin(SymRef sr) const { return isIntTimesNonlin(sr) or isRealTimesNonlin(sr); }
     bool isTimes(PTRef tr) const { return isTimes(getPterm(tr).symb()); }
-    bool isIntTimes(PTRef tr) const { return isIntTimes(getPterm(tr).symb()); }
-    bool isRealTimes(PTRef tr) const { return isRealTimes(getPterm(tr).symb()); }
+    bool isTimesLinOrNonlin(PTRef tr) const { return isTimesLinOrNonlin(getPterm(tr).symb()); };
+    bool isTimesLin(PTRef tr) const { return isTimesLin(getPterm(tr).symb()); }
+    bool isTimesNonlin(PTRef tr) const { return isTimesNonlin(getPterm(tr).symb()); }
+    bool isIntTimesLin(PTRef tr) const { return isIntTimesLin(getPterm(tr).symb()); }
+    bool isIntTimesNonlin(PTRef tr) const { return isIntTimesNonlin(getPterm(tr).symb()); }
+    bool isRealTimesLin(PTRef tr) const { return isRealTimesLin(getPterm(tr).symb()); }
+    bool isRealTimesNonlin(PTRef tr) const { return isRealTimesNonlin(getPterm(tr).symb()); }
+    bool isIntTimesLin(SymRef sr) const { return sr == sym_Int_TIMES_LIN; }
+    bool isIntTimesNonlin(SymRef sr) const { return sr == sym_Int_TIMES_NONLIN; }
+    bool isRealTimesLin(SymRef sr) const { return sr == sym_Real_TIMES_LIN; }
+    bool isRealTimesNonlin(SymRef sr) const { return sr == sym_Real_TIMES_NONLIN; }
     bool isIntTimes(SymRef sr) const { return sr == sym_Int_TIMES; }
     bool isRealTimes(SymRef sr) const { return sr == sym_Real_TIMES; }
 
@@ -222,10 +228,11 @@ class ArithLogic : public Logic {
 
     bool isNumVar(SymRef sr) const { return isVar(sr) and (yieldsSortInt(sr) or yieldsSortReal(sr)); }
     bool isNumVar(PTRef tr) const { return isNumVar(getPterm(tr).symb()); }
-    bool isNumVarLike(SymRef sr) const {
-        return yieldsSortNum(sr) and not isPlus(sr) and not isTimes(sr) and not isNumConst(sr);
+    // isMonomial property is related to PTRef only
+    bool isMonomial(PTRef tr) const {
+        SymRef sr = getPterm(tr).symb();
+        return yieldsSortNum(sr) and not isPlus(sr) and not isTimesLin(sr) and not isNumConst(sr);
     }
-    bool isNumVarLike(PTRef tr) const { return isNumVarLike(getPterm(tr).symb()); }
 
     bool isZero(SymRef sr) const { return isIntZero(sr) or isRealZero(sr); }
     bool isZero(PTRef tr) const { return isZero(getSymRef(tr)); }
@@ -267,7 +274,8 @@ class ArithLogic : public Logic {
     }
 
     SymRef getPlusForSort(SRef sort) const;
-    SymRef getTimesForSort(SRef sort) const;
+    SymRef getTimesLinForSort(SRef sort) const;
+    SymRef getTimesNonlinForSort(SRef sort) const;
     SymRef getMinusForSort(SRef sort) const;
 
     PTRef getZeroForSort(SRef sort) const;
@@ -346,7 +354,8 @@ class ArithLogic : public Logic {
     bool isLinearTerm(PTRef tr) const;
     bool isLinearFactor(PTRef tr) const;
     pair<Number, vec<PTRef>> getConstantAndFactors(PTRef sum) const;
-    pair<PTRef, PTRef> splitTermToVarAndConst(PTRef term) const;
+    // Given a term `t` is splits the term into monomial and its coefficient
+    pair<PTRef, PTRef> splitPolyTerm(PTRef term) const;
     PTRef normalizeMul(PTRef mul);
     // Given a sum term 't' returns a normalized inequality 'c <= s' equivalent to '0 <= t'
     PTRef sumToNormalizedInequality(PTRef sum);
@@ -385,6 +394,10 @@ class ArithLogic : public Logic {
     pair<Number, PTRef> sumToNormalizedIntPair(PTRef sum);
     pair<Number, PTRef> sumToNormalizedRealPair(PTRef sum);
 
+    SymRef declareFunMultiplicationLinNonlin(std::string const & s, SRef rsort, vec<SRef> const & args) {
+        return sym_store.newInternalSymb(s.c_str(), rsort, args, SymConf::CommutativeNoScopingLeftAssoc);
+    }
+
     bool hasNegativeLeadingVariable(PTRef poly) const;
 
     std::vector<Number *> numbers;
@@ -431,6 +444,8 @@ class ArithLogic : public Logic {
     SymRef sym_Real_MINUS;
     SymRef sym_Real_PLUS;
     SymRef sym_Real_TIMES;
+    SymRef sym_Real_TIMES_LIN;
+    SymRef sym_Real_TIMES_NONLIN;
     SymRef sym_Real_DIV;
     SymRef sym_Real_EQ;
     SymRef sym_Real_LEQ;
@@ -451,6 +466,8 @@ class ArithLogic : public Logic {
     SymRef sym_Int_MINUS;
     SymRef sym_Int_PLUS;
     SymRef sym_Int_TIMES;
+    SymRef sym_Int_TIMES_LIN;
+    SymRef sym_Int_TIMES_NONLIN;
     SymRef sym_Int_DIV;
     SymRef sym_Int_MOD;
     SymRef sym_Int_EQ;
diff --git a/src/logics/Logic.cc b/src/logics/Logic.cc
index 85f06522c..e7228c1cd 100644
--- a/src/logics/Logic.cc
+++ b/src/logics/Logic.cc
@@ -679,6 +679,12 @@ PTRef Logic::mkBoolVar(char const * name) {
     return mkFun(sr, {});
 }
 
+PTRef Logic::mkInternalBoolVar(char const * name) {
+    SymRef sr = declareInternalFun(name, sort_BOOL, {});
+    assert(sr != SymRef_Undef);
+    return mkFun(sr, {});
+}
+
 void Logic::instantiateFunctions(SRef sr) {
     // Equality
     SymRef tr = declareFun_Commutative_NoScoping_Chainable(tk_equals, sort_BOOL, {sr, sr});
@@ -732,8 +738,15 @@ SymRef Logic::declareFun(std::string const & fname, SRef rsort, vec<SRef> const
     assert(rsort != SRef_Undef);
     assert(std::find(args.begin(), args.end(), SRef_Undef) == args.end());
 
-    SymRef sr = sym_store.newSymb(fname.c_str(), rsort, args, symbolConfig);
-    return sr;
+    return sym_store.newSymb(fname.c_str(), rsort, args, symbolConfig);
+}
+
+SymRef Logic::declareInternalFun(std::string const & fname, SRef rsort, vec<SRef> const & args,
+                         SymbolConfig const & symbolConfig) {
+    assert(rsort != SRef_Undef);
+    assert(std::find(args.begin(), args.end(), SRef_Undef) == args.end());
+
+    return sym_store.newInternalSymb(fname.c_str(), rsort, args, symbolConfig);
 }
 
 PTRef Logic::insertTerm(SymRef sym, vec<PTRef> && terms) {
diff --git a/src/logics/Logic.h b/src/logics/Logic.h
index 9a144ee61..0625b1d01 100644
--- a/src/logics/Logic.h
+++ b/src/logics/Logic.h
@@ -164,10 +164,8 @@ class Logic {
     virtual PTRef mkConst(char const *);
     virtual PTRef mkConst(SRef, char const *);
 
-    SymRef declareFun(std::string const & fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symbolConfig);
-    SymRef declareFun(std::string const & fname, SRef rsort, vec<SRef> const & args) {
-        return declareFun(fname, rsort, args, SymConf::Default);
-    }
+    SymRef declareFun(std::string const & fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symbolConfig = SymConf::Default);
+    SymRef declareInternalFun(std::string const & fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symbolConfig = SymConf::Default);
     SymRef declareFun_NoScoping(std::string const & s, SRef rsort, vec<SRef> const & args) {
         return declareFun(s, rsort, args, SymConf::NoScoping);
     }
@@ -215,6 +213,7 @@ class Logic {
     SRef getSort(SSymRef, vec<SRef> && args);
 
     PTRef mkBoolVar(char const * name);
+    PTRef mkInternalBoolVar(char const * name);
 
     void dumpHeaderToFile(std::ostream & dump_out) const;
     void dumpFormulaToFile(std::ostream & dump_out, PTRef formula, bool negate = false, bool toassert = true) const;
diff --git a/src/parallel/ScatterSplitter.cc b/src/parallel/ScatterSplitter.cc
index 41531f841..8a78adc1d 100644
--- a/src/parallel/ScatterSplitter.cc
+++ b/src/parallel/ScatterSplitter.cc
@@ -224,7 +224,7 @@ void ScatterSplitter::exposeUnitClauses(std::vector<PTPLib::net::Lemma> & learne
 
         std::string str = logic.dumpWithLets(pt);
         assert([&](std::string_view clause_str) {
-            if (clause_str.find(".frame") != std::string::npos) {
+            if (clause_str.find(Logic::s_framev_prefix) != std::string::npos) {
                 throw PTPLib::common::Exception(__FILE__, __LINE__,"assert: frame caught in trail");
             }
             return true;
@@ -317,7 +317,7 @@ void ScatterSplitter::exposeLongerClauses(std::vector<PTPLib::net::Lemma> & lear
         std::string str = logic.dumpWithLets(theory_handler.getLogic().mkOr(clause));
         learnedLemmas.emplace_back(PTPLib::net::Lemma(str, level));
         assert([&](std::string_view clause_str) {
-            if (clause_str.find(".frame") != std::string::npos) {
+            if (clause_str.find(Logic::s_framev_prefix) != std::string::npos) {
                 throw PTPLib::common::Exception(__FILE__, __LINE__,";assert: frame caught in actual clauses");
             }
             return true;
diff --git a/src/rewriters/DivModRewriter.h b/src/rewriters/DivModRewriter.h
index 2aa90038e..6632fb90d 100644
--- a/src/rewriters/DivModRewriter.h
+++ b/src/rewriters/DivModRewriter.h
@@ -11,6 +11,7 @@
 #include "Rewriter.h"
 
 #include <common/InternalException.h>
+#include <common/NonLinException.h>
 #include <logics/ArithLogic.h>
 
 namespace opensmt {
@@ -36,6 +37,7 @@ class DivModConfig : public DefaultRewriterConfig {
             PTRef modVar = divMod.mod;
             PTRef rewritten = logic.isIntDiv(symRef) ? divVar : modVar;
             if (not inCache) {
+                if (not logic.isConstant(divisor)) { throw NonLinException(logic.pp(term)); }
                 // collect the definitions to add
                 assert(logic.isConstant(divisor));
                 auto divisorVal = logic.getNumConst(divisor);
diff --git a/src/simplifiers/LA.cc b/src/simplifiers/LA.cc
index 682c64d61..f07ad0e0d 100644
--- a/src/simplifiers/LA.cc
+++ b/src/simplifiers/LA.cc
@@ -57,14 +57,14 @@ void LAExpression::initialize(PTRef e, bool do_canonize) {
         } else if (logic.isTimes(t)) {
             // If it is times, then one side must be constant, other
             // is enqueued with a new constant
-            auto [var, constant] = logic.splitTermToVarAndConst(t);
+            auto [var, constant] = logic.splitPolyTerm(t);
             Real new_c = logic.getNumConst(constant);
             new_c *= c;
             curr_term.emplace_back(var);
             curr_const.emplace_back(std::move(new_c));
         } else {
-            // Otherwise it is a variable, Ite, UF or constant
-            assert(logic.isNumVarLike(t) || logic.isConstant(t) || logic.isUF(t));
+            // Otherwise it is a monomial or constant
+            assert(logic.isMonomial(t) || logic.isConstant(t));
             if (logic.isConstant(t)) {
                 const Real tval = logic.getNumConst(t);
                 polynome[PTRef_Undef] += tval * c;
diff --git a/src/symbols/SymStore.cc b/src/symbols/SymStore.cc
index 66cfa6051..4cd8b18e2 100644
--- a/src/symbols/SymStore.cc
+++ b/src/symbols/SymStore.cc
@@ -39,11 +39,12 @@ SymStore::~SymStore() {
         free(idToName[i]);
 }
 
-SymRef SymStore::newSymb(char const * fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symConfig) {
+SymRef SymStore::newSymbImpl(char const * fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symConfig,
+                             bool isInternal) {
     // Check if there already is a term called fname with same number of arguments of the same sort
     auto * symrefs = getRefOrNull(fname);
 
-    if (symrefs) {
+    if (symrefs && !isInternal) {
         vec<SymRef> const & trs = *symrefs;
         for (SymRef symref : trs) {
             auto const & symbol = ta[symref];
@@ -67,7 +68,7 @@ SymRef SymStore::newSymb(char const * fname, SRef rsort, vec<SRef> const & args,
         vec<SymRef> trs;
         trs.push(tr);
         symbolTable.insert(tmp_name, trs);
-    } else {
+    } else if (!isInternal) {
         symbolTable[tmp_name].push(tr); // Map the name to term reference (why not id?), used in parsing
     }
     return tr;
diff --git a/src/symbols/SymStore.h b/src/symbols/SymStore.h
index 375c8b527..e37e6bd74 100644
--- a/src/symbols/SymStore.h
+++ b/src/symbols/SymStore.h
@@ -40,9 +40,12 @@ class SymStore {
     SymStore(SymStore &&) = default;
     SymStore & operator=(SymStore &&) = default;
     // Constructs a new symbol.
-    SymRef newSymb(char const * fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symConfig);
-    SymRef newSymb(char const * fname, SRef rsort, vec<SRef> const & args) {
-        return newSymb(fname, rsort, args, SymConf::Default);
+
+    SymRef newSymb(char const * fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symConfig = SymConf::Default) {
+        return newSymbImpl(fname, rsort, args, symConfig, false);
+    };
+    SymRef newInternalSymb(char const * fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symConfig = SymConf::Default) {
+        return newSymbImpl(fname, rsort, args, symConfig, true);
     }
     bool contains(char const * fname) const { return symbolTable.has(fname); }
     vec<SymRef> const & nameToRef(char const * s) const { return symbolTable[s]; }
@@ -73,6 +76,9 @@ class SymStore {
     vec<SymRef> symbols;
     SymbolAllocator ta{1024};
     vec<char *> idToName;
+
+    SymRef newSymbImpl(char const * fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symConfig,
+                       bool isInternal);
 };
 } // namespace opensmt
 
diff --git a/src/symbols/Symbol.h b/src/symbols/Symbol.h
index 93e675b3e..191fd38b6 100644
--- a/src/symbols/Symbol.h
+++ b/src/symbols/Symbol.h
@@ -39,6 +39,7 @@ typedef uint32_t SymId; // Used as an array index
 enum class SymbolProperty : char { None, LeftAssoc, RightAssoc, Chainable, Pairwise };
 
 struct SymbolConfig {
+    //- bool isInternal;
     bool isInterpreted;
     bool commutes;
     bool noScoping;
diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc
index 1d11eaea0..98df7f3f9 100644
--- a/src/tsolvers/lasolver/LASolver.cc
+++ b/src/tsolvers/lasolver/LASolver.cc
@@ -11,6 +11,7 @@
 #include "CutCreator.h"
 
 #include <common/Random.h>
+#include <common/NonLinException.h>
 #include <models/ModelBuilder.h>
 #include <simplifiers/LA.h>
 
@@ -91,9 +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.isTimes(sum));
-    assert(!logic.isTimes(sum) || ((logic.isNumVar(logic.getPterm(sum)[0]) && logic.isOne(logic.mkNeg(logic.getPterm(sum)[1]))) ||
-                                   (logic.isNumVar(logic.getPterm(sum)[1]) && logic.isOne(logic.mkNeg(logic.getPterm(sum)[0])))));
+    assert(logic.isPlus(sum) or logic.isTimesLin(sum) or logic.isMonomial(sum));
     (void) cons; (void)sum;
 }
 
@@ -244,7 +243,7 @@ LVRef LASolver::getVarForLeq(PTRef ref) const {
 }
 
 LVRef LASolver::getLAVar_single(PTRef 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();
 
@@ -262,7 +261,7 @@ std::unique_ptr<Tableau::Polynomial> LASolver::expressionToLVarPoly(PTRef term)
     auto poly = std::make_unique<Tableau::Polynomial>();
     bool negated = laVarMapper.isNegated(term);
     for (int i = 0; i < logic.getPterm(term).size(); i++) {
-        auto [v,c] = logic.splitTermToVarAndConst(logic.getPterm(term)[i]);
+        auto [v,c] = logic.splitPolyTerm(logic.getPterm(term)[i]);
         LVRef var = getLAVar_single(v);
         Real coeff = getNum(c);
         if (negated) {
@@ -296,11 +295,11 @@ LVRef LASolver::registerArithmeticTerm(PTRef expr) {
         }
     }
 
-    if (logic.isNumVar(expr) || logic.isTimes(expr)) {
+    if (logic.isNumVar(expr) || logic.isTimesLin(expr)) {
         // Case (1), (2a), and (2b)
-        auto [v,c] = logic.splitTermToVarAndConst(expr);
-        assert(logic.isNumVar(v) || (laVarMapper.isNegated(v) && logic.isNumVar(logic.mkNeg(v))));
+        auto [v,c] = logic.splitPolyTerm(expr);
         x = getLAVar_single(v);
+        assert(logic.isNumVar(v) || (laVarMapper.isNegated(v) && logic.isNumVar(logic.mkNeg(v))));
         simplex.newNonbasicVar(x);
         notifyVar(x);
     }
@@ -847,7 +846,7 @@ std::pair<SparseLinearSystem,std::vector<PTRef>> linearSystemFromConstraints(std
         PTRef poly = defConstraint.lhs;
         fillTerms(poly, terms);
         for (PTRef arg : terms) {
-            auto [var, constant] = logic.splitTermToVarAndConst(arg);
+            auto [var, constant] = logic.splitPolyTerm(arg);
             assert(var != PTRef_Undef);
             if (varIndices.find(var) == varIndices.end()) {
                 varIndices.insert({var, columns++});
@@ -866,7 +865,7 @@ std::pair<SparseLinearSystem,std::vector<PTRef>> linearSystemFromConstraints(std
         PTRef poly = constraints[row].lhs;
         fillTerms(poly, terms);
         for (PTRef arg : terms) {
-            auto [var, constant] = logic.splitTermToVarAndConst(arg);
+            auto [var, constant] = logic.splitPolyTerm(arg);
             auto col = varIndices[var];
             columnPolynomials[col].addTerm(IndexType{row}, logic.getNumConst(constant));
         }
diff --git a/src/tsolvers/lasolver/LAVarMapper.cc b/src/tsolvers/lasolver/LAVarMapper.cc
index bcf3d95c5..e2f5fcde1 100644
--- a/src/tsolvers/lasolver/LAVarMapper.cc
+++ b/src/tsolvers/lasolver/LAVarMapper.cc
@@ -58,7 +58,7 @@ bool LAVarMapper::isNegated(PTRef tr) const {
         return false; // Case (1a)
     if (logic.isTimes(tr)) {
         // Cases (2)
-        auto [v,c] = logic.splitTermToVarAndConst(tr);
+        auto [v,c] = logic.splitPolyTerm(tr);
         return isNegated(c);
     }
     if (logic.isIte(tr)) {
diff --git a/test/regression/base/arithmetic/miniexample.smt2 b/test/regression/base/arithmetic/miniexample.smt2
new file mode 100644
index 000000000..a5c6afc70
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample.smt2
@@ -0,0 +1,5 @@
+(set-logic QF_LIA)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (* a b))
+(assert (= (uninterp_mul 1 2) 2))
+(check-sat)
+(exit)
diff --git a/test/regression/base/arithmetic/miniexample.smt2.expected.err b/test/regression/base/arithmetic/miniexample.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/arithmetic/miniexample.smt2.expected.out b/test/regression/base/arithmetic/miniexample.smt2.expected.out
new file mode 100644
index 000000000..6b8a2c3d2
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample.smt2.expected.out
@@ -0,0 +1 @@
+sat
diff --git a/test/regression/base/arithmetic/miniexample1.smt2 b/test/regression/base/arithmetic/miniexample1.smt2
new file mode 100644
index 000000000..6915ae214
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample1.smt2
@@ -0,0 +1,5 @@
+(set-logic QF_LRA)
+(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/miniexample1.smt2.expected.err b/test/regression/base/arithmetic/miniexample1.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/arithmetic/miniexample1.smt2.expected.out b/test/regression/base/arithmetic/miniexample1.smt2.expected.out
new file mode 100644
index 000000000..6b8a2c3d2
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample1.smt2.expected.out
@@ -0,0 +1 @@
+sat
diff --git a/test/regression/base/arithmetic/miniexample10.smt2 b/test/regression/base/arithmetic/miniexample10.smt2
new file mode 100644
index 000000000..53394539e
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample10.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (* 2 a b))
+(assert (= (uninterp_mul 5 x) 10))
+(check-sat)
+(get-model)
+(exit)
\ No newline at end of file
diff --git a/test/regression/base/arithmetic/miniexample10.smt2.expected.err b/test/regression/base/arithmetic/miniexample10.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/arithmetic/miniexample10.smt2.expected.out b/test/regression/base/arithmetic/miniexample10.smt2.expected.out
new file mode 100644
index 000000000..4863712af
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample10.smt2.expected.out
@@ -0,0 +1,5 @@
+sat
+(
+  (define-fun x () Int
+    1)
+)
diff --git a/test/regression/base/arithmetic/miniexample2.smt2 b/test/regression/base/arithmetic/miniexample2.smt2
new file mode 100644
index 000000000..effcb8af6
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample2.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (* a b))
+(assert (= (uninterp_mul 2 x) (+ x x)))
+(check-sat)
+(get-model)
+(exit)
\ No newline at end of file
diff --git a/test/regression/base/arithmetic/miniexample2.smt2.expected.err b/test/regression/base/arithmetic/miniexample2.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/arithmetic/miniexample2.smt2.expected.out b/test/regression/base/arithmetic/miniexample2.smt2.expected.out
new file mode 100644
index 000000000..7db85b27c
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample2.smt2.expected.out
@@ -0,0 +1,5 @@
+sat
+(
+  (define-fun x () Int
+    0)
+)
diff --git a/test/regression/base/arithmetic/miniexample3.smt2 b/test/regression/base/arithmetic/miniexample3.smt2
new file mode 100644
index 000000000..3b95f63d7
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample3.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (+ (* a b) 10))
+(assert (= (uninterp_mul y x) 30))
+(check-sat)
+(exit)
diff --git a/test/regression/base/arithmetic/miniexample3.smt2.expected.err b/test/regression/base/arithmetic/miniexample3.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/arithmetic/miniexample3.smt2.expected.out b/test/regression/base/arithmetic/miniexample3.smt2.expected.out
new file mode 100644
index 000000000..354664565
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample3.smt2.expected.out
@@ -0,0 +1 @@
+unknown
diff --git a/test/regression/base/arithmetic/miniexample3_Ok.smt2 b/test/regression/base/arithmetic/miniexample3_Ok.smt2
new file mode 100644
index 000000000..ac7406bb4
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample3_Ok.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (+ (* a b) 10))
+(assert (= (uninterp_mul y 5) 30))
+(check-sat)
+(get-model)
+(exit)
diff --git a/test/regression/base/arithmetic/miniexample3_Ok.smt2.expected.err b/test/regression/base/arithmetic/miniexample3_Ok.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/arithmetic/miniexample3_Ok.smt2.expected.out b/test/regression/base/arithmetic/miniexample3_Ok.smt2.expected.out
new file mode 100644
index 000000000..af8095222
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample3_Ok.smt2.expected.out
@@ -0,0 +1,7 @@
+sat
+(
+  (define-fun x () Int
+    0)
+  (define-fun y () Int
+    4)
+)
diff --git a/test/regression/base/arithmetic/miniexample5.smt2 b/test/regression/base/arithmetic/miniexample5.smt2
new file mode 100644
index 000000000..f1fb44dc4
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample5.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (* a (+ b 5)))
+(assert (= (uninterp_mul 2 x) (+ x 15)))
+(check-sat)
+(get-model)
+(exit)
\ No newline at end of file
diff --git a/test/regression/base/arithmetic/miniexample5.smt2.expected.err b/test/regression/base/arithmetic/miniexample5.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/arithmetic/miniexample5.smt2.expected.out b/test/regression/base/arithmetic/miniexample5.smt2.expected.out
new file mode 100644
index 000000000..cccd2f94f
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample5.smt2.expected.out
@@ -0,0 +1,5 @@
+sat
+(
+  (define-fun x () Int
+    5)
+)
diff --git a/test/regression/base/arithmetic/miniexample6.smt2 b/test/regression/base/arithmetic/miniexample6.smt2
new file mode 100644
index 000000000..57ec4e470
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample6.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (* a b))
+(assert (= (uninterp_mul x y) 10))
+(check-sat)
+(exit)
diff --git a/test/regression/base/arithmetic/miniexample6.smt2.expected.err b/test/regression/base/arithmetic/miniexample6.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/arithmetic/miniexample6.smt2.expected.out b/test/regression/base/arithmetic/miniexample6.smt2.expected.out
new file mode 100644
index 000000000..354664565
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample6.smt2.expected.out
@@ -0,0 +1 @@
+unknown
diff --git a/test/regression/base/arithmetic/miniexample6_Ok.smt2 b/test/regression/base/arithmetic/miniexample6_Ok.smt2
new file mode 100644
index 000000000..61cc3b630
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample6_Ok.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (* a b))
+(assert (= (uninterp_mul x 10) y))
+(check-sat)
+(get-model)
+(exit)
diff --git a/test/regression/base/arithmetic/miniexample6_Ok.smt2.expected.err b/test/regression/base/arithmetic/miniexample6_Ok.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/arithmetic/miniexample6_Ok.smt2.expected.out b/test/regression/base/arithmetic/miniexample6_Ok.smt2.expected.out
new file mode 100644
index 000000000..ebf63a539
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample6_Ok.smt2.expected.out
@@ -0,0 +1,7 @@
+sat
+(
+  (define-fun x () Int
+    0)
+  (define-fun y () Int
+    0)
+)
diff --git a/test/regression/base/arithmetic/miniexample7.smt2 b/test/regression/base/arithmetic/miniexample7.smt2
new file mode 100644
index 000000000..989cc24de
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample7.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (div a b))
+(assert (= (uninterp_mul x y) 10))
+(check-sat)
+(exit)
diff --git a/test/regression/base/arithmetic/miniexample7.smt2.expected.err b/test/regression/base/arithmetic/miniexample7.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/arithmetic/miniexample7.smt2.expected.out b/test/regression/base/arithmetic/miniexample7.smt2.expected.out
new file mode 100644
index 000000000..354664565
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample7.smt2.expected.out
@@ -0,0 +1 @@
+unknown
diff --git a/test/regression/base/arithmetic/miniexample7_Ok.smt2 b/test/regression/base/arithmetic/miniexample7_Ok.smt2
new file mode 100644
index 000000000..68ffd95aa
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample7_Ok.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (div a b))
+(assert (= (uninterp_mul 10 y) x))
+(check-sat)
+(exit)
diff --git a/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.err b/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out b/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out
new file mode 100644
index 000000000..354664565
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out
@@ -0,0 +1 @@
+unknown
diff --git a/test/regression/base/arithmetic/miniexample7_Ok1.smt2 b/test/regression/base/arithmetic/miniexample7_Ok1.smt2
new file mode 100644
index 000000000..36c908178
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample7_Ok1.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (div a b))
+(assert (= (uninterp_mul y 10) x))
+(check-sat)
+(get-model)
+(exit)
diff --git a/test/regression/base/arithmetic/miniexample7_Ok1.smt2.expected.err b/test/regression/base/arithmetic/miniexample7_Ok1.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/arithmetic/miniexample7_Ok1.smt2.expected.out b/test/regression/base/arithmetic/miniexample7_Ok1.smt2.expected.out
new file mode 100644
index 000000000..ebf63a539
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample7_Ok1.smt2.expected.out
@@ -0,0 +1,7 @@
+sat
+(
+  (define-fun x () Int
+    0)
+  (define-fun y () Int
+    0)
+)
diff --git a/test/regression/base/arithmetic/miniexample8.smt2 b/test/regression/base/arithmetic/miniexample8.smt2
new file mode 100644
index 000000000..9a09e5260
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample8.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (mod a b))
+(assert (= (uninterp_mul x y) 0))
+(check-sat)
+(exit)
\ No newline at end of file
diff --git a/test/regression/base/arithmetic/miniexample8.smt2.expected.err b/test/regression/base/arithmetic/miniexample8.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/arithmetic/miniexample8.smt2.expected.out b/test/regression/base/arithmetic/miniexample8.smt2.expected.out
new file mode 100644
index 000000000..354664565
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample8.smt2.expected.out
@@ -0,0 +1 @@
+unknown
diff --git a/test/regression/base/arithmetic/miniexample8_Ok.smt2 b/test/regression/base/arithmetic/miniexample8_Ok.smt2
new file mode 100644
index 000000000..8d277d485
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample8_Ok.smt2
@@ -0,0 +1,5 @@
+(set-logic QF_LIA)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (mod a b))
+(assert (= (uninterp_mul 1 2) 0))
+(check-sat)
+(exit)
\ No newline at end of file
diff --git a/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.err b/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.out b/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.out
new file mode 100644
index 000000000..3f65111b0
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.out
@@ -0,0 +1 @@
+unsat
diff --git a/test/regression/base/arithmetic/miniexample8_Ok2.smt2 b/test/regression/base/arithmetic/miniexample8_Ok2.smt2
new file mode 100644
index 000000000..741ce62af
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample8_Ok2.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (mod a b))
+(assert (= (uninterp_mul x 5) 0))
+(check-sat)
+(exit)
\ No newline at end of file
diff --git a/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.err b/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.out b/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.out
new file mode 100644
index 000000000..6b8a2c3d2
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.out
@@ -0,0 +1 @@
+sat
diff --git a/test/regression/base/arithmetic/miniexample9.smt2 b/test/regression/base/arithmetic/miniexample9.smt2
new file mode 100644
index 000000000..45c07977b
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample9.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (mod a b))
+(assert (= (uninterp_mul 5 x) 0))
+(check-sat)
+(exit)
\ No newline at end of file
diff --git a/test/regression/base/arithmetic/miniexample9.smt2.expected.err b/test/regression/base/arithmetic/miniexample9.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/arithmetic/miniexample9.smt2.expected.out b/test/regression/base/arithmetic/miniexample9.smt2.expected.out
new file mode 100644
index 000000000..354664565
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample9.smt2.expected.out
@@ -0,0 +1 @@
+unknown
diff --git a/test/unit/test_ArithLogicApi.cc b/test/unit/test_ArithLogicApi.cc
index ddc7dbb8e..0ec854b7d 100644
--- a/test/unit/test_ArithLogicApi.cc
+++ b/test/unit/test_ArithLogicApi.cc
@@ -4,7 +4,6 @@
 
 #include <gtest/gtest.h>
 #include <logics/ArithLogic.h>
-#include <common/StringConv.h>
 
 namespace opensmt {
 
@@ -28,7 +27,7 @@ TEST_F(ArithLogicApiTest, test_LRA) {
     ASSERT_TRUE(lraLogic.yieldsSortReal(r1));
     PTRef c2 = lraLogic.mkRealVar("a");
     ASSERT_NO_THROW(lraLogic.mkPlus(c1, c2));
-    ASSERT_THROW(lraLogic.mkTimes(c2, c2), LANonLinearException);
+    ASSERT_NO_THROW(lraLogic.mkTimes(c2, c2));
     ASSERT_THROW(lraLogic.mkIntVar("x"), ApiException);
     ASSERT_THROW(lraLogic.mkIntConst(2), ApiException);
 }
@@ -39,7 +38,7 @@ TEST_F(ArithLogicApiTest, test_LIA) {
     ASSERT_THROW(liaLogic.mkConst("213.0"), ApiException);
     PTRef c2 = liaLogic.mkIntVar("a");
     ASSERT_NO_THROW(liaLogic.mkPlus(c1, c2));
-    ASSERT_THROW(liaLogic.mkTimes(c2, c2), LANonLinearException);
+    ASSERT_NO_THROW(liaLogic.mkTimes(c2, c2));
     ASSERT_THROW(liaLogic.mkRealVar("a"), ApiException);
     ASSERT_THROW(liaLogic.mkRealConst(2), ApiException);
 }
diff --git a/test/unit/test_Ites.cc b/test/unit/test_Ites.cc
index ff3e5b41f..2a37bc126 100644
--- a/test/unit/test_Ites.cc
+++ b/test/unit/test_Ites.cc
@@ -136,12 +136,11 @@ TEST_F(IteManagerTest, test_IteTimesVar) {
     PTRef c2 = logic.mkConst("2");
     PTRef ite = logic.mkIte(cond, c1, c2);
 
-    EXPECT_THROW(logic.mkTimes(ite, x), LANonLinearException);
+    EXPECT_NO_THROW(logic.mkTimes(ite, x));
 
 }
 
 TEST_F(IteManagerTest, test_IteTimesIte) {
-
     PTRef x = logic.mkVar(lrasort, "x");
     PTRef y = logic.mkVar(lrasort, "y");
     PTRef z = logic.mkVar(lrasort, "z");
@@ -153,7 +152,7 @@ TEST_F(IteManagerTest, test_IteTimesIte) {
     PTRef cond2 = logic.mkEq(x, z);
     PTRef ite2 = logic.mkIte(cond2, c2, c1);
 
-    EXPECT_THROW(logic.mkTimes(ite1, ite2), LANonLinearException);
+    EXPECT_NO_THROW(logic.mkTimes(ite1, ite2));
 }
 
 TEST_F(IteManagerTest, test_IteChain) {
diff --git a/test/unit/test_LIALogicMkTerms.cc b/test/unit/test_LIALogicMkTerms.cc
index 8d6ed42e1..f41d12ce2 100644
--- a/test/unit/test_LIALogicMkTerms.cc
+++ b/test/unit/test_LIALogicMkTerms.cc
@@ -74,7 +74,7 @@ TEST_F(LIALogicMkTermsTest, testMod_Times) {
     PTRef three = logic.mkIntConst(3);
     PTRef mod = logic.mkMod(x,two);
     PTRef times = logic.mkTimes(mod, three);
-    EXPECT_EQ(logic.getSymRef(times), logic.get_sym_Int_TIMES());
+    EXPECT_EQ(logic.getSymRef(times), logic.get_sym_Int_TIMES_LIN());
 }
 
 TEST_F(LIALogicMkTermsTest, testMod_Leq) {
@@ -191,8 +191,8 @@ TEST_F(LIALogicMkTermsTest, test_EqualityNormalization_EqualityToConstant) {
     PTRef eq = logic.mkEq(x, two);
     PTRef lhs = logic.getPterm(eq)[0];
     PTRef rhs = logic.getPterm(eq)[1];
-    EXPECT_NE(logic.getSymRef(lhs), logic.get_sym_Int_TIMES());
-    EXPECT_NE(logic.getSymRef(rhs), logic.get_sym_Int_TIMES());
+    EXPECT_NE(logic.getSymRef(lhs), logic.get_sym_Int_TIMES_LIN());
+    EXPECT_NE(logic.getSymRef(rhs), logic.get_sym_Int_TIMES_LIN());
 }
 
 TEST_F(LIALogicMkTermsTest, test_ReverseAuxRewrite) {
diff --git a/test/unit/test_LRALogicMkTerms.cc b/test/unit/test_LRALogicMkTerms.cc
index 03567c88a..4d1d6d068 100644
--- a/test/unit/test_LRALogicMkTerms.cc
+++ b/test/unit/test_LRALogicMkTerms.cc
@@ -173,9 +173,9 @@ TEST_F(LRALogicMkTermsTest, test_SumToZero)
     ASSERT_EQ(sum, logic.getTerm_RealZero());
 }
 
-TEST_F(LRALogicMkTermsTest, test_NonLinearException)
+TEST_F(LRALogicMkTermsTest, test_NoNonLinearException)
 {
-    EXPECT_THROW(logic.mkTimes(x,y), LANonLinearException);
+    EXPECT_NO_THROW(logic.mkTimes(x,y));
     PTRef two = logic.mkConst("2");
     EXPECT_NO_THROW(logic.mkTimes(x,two));
 }