diff --git a/regression/ebmc-spot/sva-buechi/sequence_first_match1.desc b/regression/ebmc-spot/sva-buechi/sequence_first_match1.desc
deleted file mode 100644
index df05c054a..000000000
--- a/regression/ebmc-spot/sva-buechi/sequence_first_match1.desc
+++ /dev/null
@@ -1,11 +0,0 @@
-CORE
-../../verilog/SVA/sequence_first_match1.sv
---buechi --bound 5
-^error: failed to convert sva_sequence_first_match$
-^EXIT=6$
-^SIGNAL=0$
---
-^warning: ignoring
-^\[.*\] first_match\(main\.x == 0\): PROVED up to bound 5$
-^\[.*\] first_match\(main\.x == 0, main\.x\+\+\): PROVED up to bound 5$
---
diff --git a/regression/ebmc-spot/sva-buechi/sequence_first_match1.k.desc b/regression/ebmc-spot/sva-buechi/sequence_first_match1.k.desc
new file mode 100644
index 000000000..42068cc34
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/sequence_first_match1.k.desc
@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/sequence_first_match1.sv
+--buechi --k-induction --bound 1
+^\[.*\] first_match\(main\.x == 0\): PROVED$
+^\[.*\] first_match\(main\.x == 0, main\.x\+\+\): PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc-spot/sva-buechi/sequence_first_match2.desc b/regression/ebmc-spot/sva-buechi/sequence_first_match2.k.desc
similarity index 59%
rename from regression/ebmc-spot/sva-buechi/sequence_first_match2.desc
rename to regression/ebmc-spot/sva-buechi/sequence_first_match2.k.desc
index 35c642a6b..73c25b911 100644
--- a/regression/ebmc-spot/sva-buechi/sequence_first_match2.desc
+++ b/regression/ebmc-spot/sva-buechi/sequence_first_match2.k.desc
@@ -1,13 +1,12 @@
 CORE
 ../../verilog/SVA/sequence_first_match2.sv
---buechi --bound 5
-^error: failed to convert sva_sequence_first_match$
-^EXIT=6$
-^SIGNAL=0$
---
+--buechi --k-induction --bound 2
 ^\[.*\] \(\(##1 1\) or \(##2 1\)\) \|-> main.x == 1: REFUTED$
-^\[.*\] first_match\(\(##1 1\) or \(##2 1\)\) \|-> main\.x == 1: PROVED up to bound 5$
+^\[.*\] first_match\(\(##1 1\) or \(##2 1\)\) \|-> main\.x == 1: PROVED$
 ^\[.*\] \(1 or \(##1 1\)\) \|-> main\.x == 0: REFUTED$
-^\[.*\] first_match\(1 or \(##1 1\)\) \|-> main\.x == 0: PROVED up to bound 5$
+^\[.*\] first_match\(1 or \(##1 1\)\) \|-> main\.x == 0: PROVED$
+^EXIT=10$
+^SIGNAL=0$
+--
 ^warning: ignoring
 --
diff --git a/src/temporal-logic/ltl_sva_to_string.cpp b/src/temporal-logic/ltl_sva_to_string.cpp
index f69b97352..8b3f00cda 100644
--- a/src/temporal-logic/ltl_sva_to_string.cpp
+++ b/src/temporal-logic/ltl_sva_to_string.cpp
@@ -546,6 +546,13 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
       DATA_INVARIANT(
         false, "unexpected sva_sequence_non_consecutive_repetition");
   }
+  else if(expr.id() == ID_sva_sequence_first_match) // first_match(...)
+  {
+    PRECONDITION(mode == SVA_SEQUENCE);
+    auto &sequence = to_sva_sequence_first_match_expr(expr).sequence();
+    auto op_rec = rec(sequence, SVA_SEQUENCE);
+    return resultt{precedencet::ATOM, "first_match(" + op_rec.s + ')'};
+  }
   else if(!is_temporal_operator(expr))
   {
     auto number = atoms.number(expr);