diff --git a/integration_test/Target/ExportSMTLIB/attributes.mlir b/integration_test/Target/ExportSMTLIB/attributes.mlir
index e24a311118..555bb7d577 100644
--- a/integration_test/Target/ExportSMTLIB/attributes.mlir
+++ b/integration_test/Target/ExportSMTLIB/attributes.mlir
@@ -20,4 +20,4 @@ smt.solver () : () -> () {
 // CHECK-NOT: ERROR
 // CHECK-NOT: error
 // CHECK-NOT: unsat
-// CHECK: sat
\ No newline at end of file
+// CHECK: sat
diff --git a/lib/Target/ExportSMTLIB/ExportSMTLIB.cpp b/lib/Target/ExportSMTLIB/ExportSMTLIB.cpp
index 27c14699c2..4446bb2227 100644
--- a/lib/Target/ExportSMTLIB/ExportSMTLIB.cpp
+++ b/lib/Target/ExportSMTLIB/ExportSMTLIB.cpp
@@ -158,7 +158,7 @@ struct ExpressionVisitor
     info.stream << "(let ((" << name << " ";
 
     VisitorInfo newInfo(info.stream, info.valueMap,
-                        info.indentLevel + 7 + name.size(), info.openParens);
+                        info.indentLevel + 8 + name.size(), 0);
     if (failed(Base::dispatchSMTOpVisitor(op, newInfo)))
       return failure();
 
@@ -332,14 +332,14 @@ struct ExpressionVisitor
     worklist.push_back(yieldedValue);
     unsigned indentExt = operatorString.size() + 2;
     VisitorInfo newInfo(info.stream, info.valueMap,
-                        info.indentLevel + indentExt, info.openParens);
+                        info.indentLevel + indentExt, 0);
     newInfo.stream.indent(newInfo.indentLevel);
     if (failed(printExpression(worklist, newInfo)))
       return failure();
 
     info.stream << info.valueMap.lookup(yieldedValue);
 
-    for (int j = 0; j < newInfo.openParens; ++j)
+    for (unsigned j = 0; j < newInfo.openParens; ++j)
       info.stream << ")";
 
     if (weight != 0)
diff --git a/test/Target/ExportSMTLIB/attributes.mlir b/test/Target/ExportSMTLIB/attributes.mlir
index 988d43fe20..ce34c48f45 100644
--- a/test/Target/ExportSMTLIB/attributes.mlir
+++ b/test/Target/ExportSMTLIB/attributes.mlir
@@ -52,4 +52,4 @@ smt.solver () : () -> () {
 
   // CHECK: (reset)
   // CHECK-INLINED: (reset)
-}
\ No newline at end of file
+}
diff --git a/test/Target/ExportSMTLIB/core.mlir b/test/Target/ExportSMTLIB/core.mlir
index ebcfe7acc9..d855137d4b 100644
--- a/test/Target/ExportSMTLIB/core.mlir
+++ b/test/Target/ExportSMTLIB/core.mlir
@@ -89,6 +89,29 @@ smt.solver () : () -> () {
   }
   smt.assert %2
 
+  // Test: make sure that open parens from outside quantifier bodies are not
+  // propagated into the body.
+  // CHECK: (assert (let (([[V15:.+]] (exists (([[V16:.+]] Int) ([[V17:.+]] Int)){{$}}
+  // CHECK:                                   (let (([[V18:.+]] (= [[V16]] [[V17]]))){{$}}
+  // CHECK:                                   [[V18]])))){{$}}
+  // CHECK:         (let (([[V19:.+]] (exists (([[V20:.+]] Int) ([[V21:.+]] Int)){{$}}
+  // CHECK:                                   (let (([[V22:.+]] (= [[V20]] [[V21]]))){{$}}
+  // CHECK:                                   [[V22]])))){{$}}
+  // CHECK:         (let (([[V23:.+]] (and [[V19]] [[V15]]))){{$}}
+  // CHECK:         [[V23]])))){{$}}
+  %3 = smt.exists {
+  ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+    %5 = smt.eq %arg2, %arg3 : !smt.int
+    smt.yield %5 : !smt.bool
+  }
+  %5 = smt.exists {
+  ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+    %6 = smt.eq %arg2, %arg3 : !smt.int
+    smt.yield %6 : !smt.bool
+  }
+  %6 = smt.and %3, %5
+  smt.assert %6
+
   // CHECK: (check-sat)
   // CHECK-INLINED: (check-sat)
   smt.check sat {} unknown {} unsat {}