1 files changed, 13 insertions, 10 deletions
diff --git a/src/test/scala/firrtl/backends/experimental/smt/SMTLibSpec.scala b/src/test/scala/firrtl/backends/experimental/smt/SMTLibSpec.scala
index b970484e..338d760c 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/SMTLibSpec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/SMTLibSpec.scala
@@ -2,7 +2,10 @@
 
 package firrtl.backends.experimental.smt
 
-private class SMTLibSpec extends SMTBackendBaseSpec {
+import org.scalatest.flatspec.AnyFlatSpec
+
+class SMTLibSpec extends AnyFlatSpec {
+  behavior.of("SMTLib backend")
 
   it should "convert a hello world module" in {
     val src =
@@ -12,7 +15,7 @@ private class SMTLibSpec extends SMTBackendBaseSpec {
         |    input a: UInt<8>
         |    output b: UInt<16>
         |    b <= a
-        |    assert(clock, eq(a, b), UInt(1), "")
+        |    assert(clock, eq(a, b), UInt(1), "") : a_eq_b
         |""".stripMargin
 
     val expected =
@@ -21,15 +24,15 @@ private class SMTLibSpec extends SMTBackendBaseSpec {
         |(declare-fun a_f (m_s) (_ BitVec 8))
         |; firrtl-smt2-output b 16
         |(define-fun b_f ((state m_s)) (_ BitVec 16) ((_ zero_extend 8) (a_f state)))
-        |; firrtl-smt2-assert assert_ 1
-        |(define-fun assert__f ((state m_s)) Bool (= ((_ zero_extend 8) (a_f state)) (b_f state)))
+        |; firrtl-smt2-assert a_eq_b 1
+        |(define-fun a_eq_b_f ((state m_s)) Bool (= ((_ zero_extend 8) (a_f state)) (b_f state)))
         |(define-fun m_t ((state m_s) (state_n m_s)) Bool true)
         |(define-fun m_i ((state m_s)) Bool true)
-        |(define-fun m_a ((state m_s)) Bool (assert__f state))
+        |(define-fun m_a ((state m_s)) Bool (a_eq_b_f state))
         |(define-fun m_u ((state m_s)) Bool true)
         |""".stripMargin
 
-    assert(toSMTLibStr(src) == expected)
+    assert(SMTBackendHelpers.toSMTLibStr(src) == expected)
   }
 
   it should "include FileInfo in the output" in {
@@ -52,15 +55,15 @@ private class SMTLibSpec extends SMTBackendBaseSpec {
         |; firrtl-smt2-output b 16
         |; @ b 0:0, b_a 0:0
         |(define-fun b_f ((state m_s)) (_ BitVec 16) ((_ zero_extend 8) (a_f state)))
-        |; firrtl-smt2-assert assert_ 1
+        |; firrtl-smt2-assert assert_0 1
         |; @ assert 0:0
-        |(define-fun assert__f ((state m_s)) Bool (= ((_ zero_extend 8) (a_f state)) (b_f state)))
+        |(define-fun assert_0_f ((state m_s)) Bool (= ((_ zero_extend 8) (a_f state)) (b_f state)))
         |(define-fun m_t ((state m_s) (state_n m_s)) Bool true)
         |(define-fun m_i ((state m_s)) Bool true)
-        |(define-fun m_a ((state m_s)) Bool (assert__f state))
+        |(define-fun m_a ((state m_s)) Bool (assert_0_f state))
         |(define-fun m_u ((state m_s)) Bool true)
         |""".stripMargin
 
-    assert(toSMTLibStr(src) == expected)
+    assert(SMTBackendHelpers.toSMTLibStr(src) == expected)
   }
 }