update

Author: keram88

lib/smack/Prelude.cpp

@@ -1591,10 +1591,13 @@ void FpOpGen::generateConvOps(std::stringstream &s) const {
       auto exp = FP_LAYOUT.at(bw).first;
       auto sig = FP_LAYOUT.at(bw).second;
       std::string type = getFpTypeName(bw);
-      s << uninterpretedOp("$fpext", {type, "float"}, makeFpVars(1, 0), "float") << "\n";
-      s << uninterpretedOp("$fptrunc", {type, "float"}, makeFpVars(1, 0), "float") << "\n";
-      s << uninterpretedOp("$fpext", {"float", type}, makeFpVars(1, 0), type) << "\n";
-      s << uninterpretedOp("$fptrunc", {"float", type}, makeFpVars(1, 0), type) << "\n";
+      std::list<Binding> bs = makeFpVars(1, srcBw);
+
+      bs.insert(bs.begin(), {makeRMODEVarName(), getRMODETypeName()});
+      s << uninterpretedOp("$fpext", {type, "float"}, bs, "float") << "\n";
+      s << uninterpretedOp("$fptrunc", {type, "float"}, bs, "float") << "\n";
+      s << uninterpretedOp("$fpext", {"float", type}, bs, type) << "\n";
+      s << uninterpretedOp("$fptrunc", {"float", type}, bs, type) << "\n";
     }
   }
 }