diff --git a/src/library/compiler/csimp.cpp b/src/library/compiler/csimp.cpp
index b24c3a6acb..825a940f7c 100644
--- a/src/library/compiler/csimp.cpp
+++ b/src/library/compiler/csimp.cpp
@@ -471,6 +471,21 @@ class csimp_fn {
             e_y = *e_y_opt;
         }
         expr new_jp_val  = e_y;
+        /* Some of the new join points in `new_jps` may be replacing join points defined at jp_decl.
+           So, we must insert them after the old one, and remove them from `new_jps` and `new_jp_cache`. */
+        unsigned i = saved_fvars_size;
+        while (i < m_fvars.size()) {
+            expr curr = m_fvars[i];
+            auto it = new_jp_cache.find(curr);
+            if (it != new_jp_cache.end()) {
+                m_fvars.insert(i+i, it->second);
+                new_jp_cache.erase(curr);
+                new_jps.erase_elem(curr);
+                i = i + 2;
+            } else {
+                i = i + 1;
+            }
+        }
         new_jp_val = mk_let(saved_fvars_size, new_jp_val);
         new_jp_val = m_lctx.mk_lambda(zs, new_jp_val);
         mark_simplified(new_jp_val);