diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 49b5f988f..1b4b1e7bc 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -770,7 +770,7 @@ namespace opt {
                   tout << "offset: " << offset << "\n";
                   );
             std::ostringstream out;
-            out << mk_pp(orig_term, m);
+            out << mk_pp(orig_term, m) << ":" << index;
             id = symbol(out.str().c_str());
             return true;
         }
@@ -793,7 +793,7 @@ namespace opt {
             }
             neg = true;
             std::ostringstream out;
-            out << mk_pp(orig_term, m);
+            out << mk_pp(orig_term, m) << ":" << index;
             id = symbol(out.str().c_str());
             return true;
         }
@@ -812,7 +812,7 @@ namespace opt {
             }
             neg = is_max;
             std::ostringstream out;
-            out << mk_pp(orig_term, m);
+            out << mk_pp(orig_term, m) << ":" << index;
             id = symbol(out.str().c_str());
             return true;            
         }