diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp
index 268085090..2f7fe1be2 100755
--- a/src/interp/iz3mgr.cpp
+++ b/src/interp/iz3mgr.cpp
@@ -733,6 +733,8 @@ void iz3mgr::linear_comb(ast &P, const ast &c, const ast &Q, bool round_off){
         }
     }
     bool pstrict = op(P) == Lt;
+    if (round_off && get_type(Qrhs) != int_type())
+        round_off = false;
     if(qstrict && round_off && (pstrict || !(c == make_int(rational(1))))){
         Qrhs = make(Sub,Qrhs,make_int(rational(1)));
         qstrict = false;
diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp
index 2b4100e5e..046b0b7f1 100755
--- a/src/interp/iz3proof_itp.cpp
+++ b/src/interp/iz3proof_itp.cpp
@@ -2584,6 +2584,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
         if(pstrict && qstrict && round_off)
             Qrhs = make(Sub,Qrhs,make_int(rational(1)));
 #else
+        if (round_off && get_type(Qrhs) != int_type())
+            round_off = false;
         bool pstrict = op(P) == Lt;
         if(qstrict && round_off && (pstrict || !(c == make_int(rational(1))))){
             Qrhs = make(Sub,Qrhs,make_int(rational(1)));