From fde07ab5b57448b069078998fd52a29543fd5a73 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Thu, 2 May 2024 14:11:29 -0400
Subject: [PATCH] SMV frontend: strip main:: from property pretty names

The SMV namespace always has main as its root; strip it from the pretty
names of properties.
---
 regression/ebmc/BDD/AF1.desc                     |  4 ++--
 regression/ebmc/BDD/AF2.desc                     |  4 ++--
 regression/ebmc/BDD/AG1.desc                     |  4 ++--
 regression/ebmc/BDD/AG2.desc                     |  4 ++--
 regression/ebmc/BDD/AX1.desc                     |  4 ++--
 regression/ebmc/BDD/BDD1.desc                    |  2 +-
 regression/ebmc/BDD/BDD4.desc                    |  2 +-
 regression/ebmc/BDD/BDD5.desc                    |  2 +-
 regression/ebmc/BDD/EF1.desc                     |  4 ++--
 regression/ebmc/BDD/EF2.desc                     |  4 ++--
 regression/ebmc/BDD/EG1.desc                     |  4 ++--
 regression/ebmc/BDD/EG2.desc                     |  4 ++--
 regression/ebmc/BDD/EX1.desc                     |  4 ++--
 regression/ebmc/BDD/EX2.desc                     |  4 ++--
 regression/ebmc/BDD/GF1.desc                     |  2 +-
 regression/ebmc/BDD/just_p.desc                  |  4 ++--
 regression/ebmc/Properties1/test.desc            |  6 +++---
 regression/ebmc/elbtunnel/test.desc              | 16 ++++++++--------
 regression/ebmc/range_type/range_type1.desc      |  2 +-
 regression/ebmc/range_type/range_type2.desc      |  4 ++--
 regression/ebmc/range_type/range_type3.desc      |  2 +-
 regression/ebmc/range_type/range_type4.desc      |  2 +-
 regression/ebmc/range_type/range_type5.desc      |  2 +-
 regression/ebmc/small-test1/test.desc            |  2 +-
 regression/ebmc/small-test2/test.desc            |  2 +-
 .../ebmc/smv/bdd_unsupported_property.desc       |  4 ++--
 .../ebmc/smv/bmc_unsupported_property1.desc      |  4 ++--
 .../ebmc/smv/bmc_unsupported_property2.desc      |  4 ++--
 .../ebmc/smv/bmc_unsupported_property3.desc      |  4 ++--
 regression/ebmc/smv/initial1.desc                |  4 ++--
 regression/ebmc/smv/smv1.desc                    |  2 +-
 regression/ebmc/smv/smv2.desc                    |  2 +-
 regression/ebmc/smv/smv3.desc                    |  2 +-
 regression/ebmc/smv/smv_ltlspec1.desc            |  2 +-
 regression/ebmc/smv/smv_ltlspec2.desc            |  2 +-
 regression/ebmc/smv/smv_ltlspec3.desc            |  2 +-
 regression/ebmc/smv/smv_ltlspec4.desc            |  4 ++--
 regression/ebmc/traces/numbered1.desc            |  2 +-
 regression/ebmc/traces/waveform1.desc            |  2 +-
 src/smvlang/smv_typecheck.cpp                    | 10 +++++++---
 40 files changed, 74 insertions(+), 70 deletions(-)

diff --git a/regression/ebmc/BDD/AF1.desc b/regression/ebmc/BDD/AF1.desc
index fee19fe3e..9c9c96562 100644
--- a/regression/ebmc/BDD/AF1.desc
+++ b/regression/ebmc/BDD/AF1.desc
@@ -1,8 +1,8 @@
 CORE
 AF1.smv
 --bdd
-^\[main::spec1\] AF some_var = TRUE: REFUTED$
-^\[main::spec2\] AF some_var = FALSE: PROVED$
+^\[spec1\] AF some_var = TRUE: REFUTED$
+^\[spec2\] AF some_var = FALSE: PROVED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/AF2.desc b/regression/ebmc/BDD/AF2.desc
index 9a274ca3c..2178f72a0 100644
--- a/regression/ebmc/BDD/AF2.desc
+++ b/regression/ebmc/BDD/AF2.desc
@@ -1,8 +1,8 @@
 CORE
 AF2.smv
 --bdd
-^\[main::spec1\] AF some_var = TRUE: REFUTED$
-^\[main::spec2\] AF some_var = FALSE: PROVED$
+^\[spec1\] AF some_var = TRUE: REFUTED$
+^\[spec2\] AF some_var = FALSE: PROVED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/AG1.desc b/regression/ebmc/BDD/AG1.desc
index 0ab3b01ee..da4a060d4 100644
--- a/regression/ebmc/BDD/AG1.desc
+++ b/regression/ebmc/BDD/AG1.desc
@@ -1,8 +1,8 @@
 CORE
 AG1.smv
 --bdd
-^\[main::spec1\] AG some_var = TRUE: REFUTED$
-^\[main::spec2\] AG some_var = FALSE: PROVED$
+^\[spec1\] AG some_var = TRUE: REFUTED$
+^\[spec2\] AG some_var = FALSE: PROVED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/AG2.desc b/regression/ebmc/BDD/AG2.desc
index aed42a6e6..b3dc54b91 100644
--- a/regression/ebmc/BDD/AG2.desc
+++ b/regression/ebmc/BDD/AG2.desc
@@ -1,8 +1,8 @@
 CORE
 AG2.smv
 --bdd
-^\[main::spec1\] AG some_var = TRUE: REFUTED$
-^\[main::spec2\] AG some_var = FALSE: REFUTED$
+^\[spec1\] AG some_var = TRUE: REFUTED$
+^\[spec2\] AG some_var = FALSE: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/AX1.desc b/regression/ebmc/BDD/AX1.desc
index abc4ce68d..6388702e3 100644
--- a/regression/ebmc/BDD/AX1.desc
+++ b/regression/ebmc/BDD/AX1.desc
@@ -1,8 +1,8 @@
 CORE
 AX1.smv
 --bdd
-^\[main::spec1\] AX some_var = TRUE: REFUTED$
-^\[main::spec2\] AX some_var = FALSE: PROVED$
+^\[spec1\] AX some_var = TRUE: REFUTED$
+^\[spec2\] AX some_var = FALSE: PROVED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/BDD1.desc b/regression/ebmc/BDD/BDD1.desc
index 649e39aa2..928e3b753 100644
--- a/regression/ebmc/BDD/BDD1.desc
+++ b/regression/ebmc/BDD/BDD1.desc
@@ -3,6 +3,6 @@ BDD1.smv
 --bdd
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec1\] AG \(!some_var = off\): PROVED$
+^\[spec1\] AG \(!some_var = off\): PROVED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/BDD/BDD4.desc b/regression/ebmc/BDD/BDD4.desc
index ab2fd6eb7..2c24d5fd9 100644
--- a/regression/ebmc/BDD/BDD4.desc
+++ b/regression/ebmc/BDD/BDD4.desc
@@ -3,6 +3,6 @@ BDD4.smv
 --bdd
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] AG .*: REFUTED$
+^\[spec1\] AG .*: REFUTED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/BDD/BDD5.desc b/regression/ebmc/BDD/BDD5.desc
index 6e27db1b2..c8d3d2016 100644
--- a/regression/ebmc/BDD/BDD5.desc
+++ b/regression/ebmc/BDD/BDD5.desc
@@ -3,6 +3,6 @@ BDD5.smv
 --bdd
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec1\] AG .*: PROVED$
+^\[spec1\] AG .*: PROVED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/BDD/EF1.desc b/regression/ebmc/BDD/EF1.desc
index 8da7b9529..b7a694b2e 100644
--- a/regression/ebmc/BDD/EF1.desc
+++ b/regression/ebmc/BDD/EF1.desc
@@ -1,8 +1,8 @@
 CORE
 EF1.smv
 --bdd
-^\[main::spec1\] EF some_var = TRUE: REFUTED$
-^\[main::spec2\] EF some_var = FALSE: PROVED$
+^\[spec1\] EF some_var = TRUE: REFUTED$
+^\[spec2\] EF some_var = FALSE: PROVED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/EF2.desc b/regression/ebmc/BDD/EF2.desc
index ce03ac682..5a2f029d1 100644
--- a/regression/ebmc/BDD/EF2.desc
+++ b/regression/ebmc/BDD/EF2.desc
@@ -1,8 +1,8 @@
 CORE
 EF2.smv
 --bdd
-^\[main::spec1\] EF some_var = TRUE: REFUTED$
-^\[main::spec2\] EF some_var = FALSE: PROVED$
+^\[spec1\] EF some_var = TRUE: REFUTED$
+^\[spec2\] EF some_var = FALSE: PROVED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/EG1.desc b/regression/ebmc/BDD/EG1.desc
index d76c69604..69c810b5e 100644
--- a/regression/ebmc/BDD/EG1.desc
+++ b/regression/ebmc/BDD/EG1.desc
@@ -1,8 +1,8 @@
 CORE
 EG1.smv
 --bdd
-^\[main::spec1\] EG some_var = TRUE: REFUTED$
-^\[main::spec2\] EG some_var = FALSE: PROVED$
+^\[spec1\] EG some_var = TRUE: REFUTED$
+^\[spec2\] EG some_var = FALSE: PROVED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/EG2.desc b/regression/ebmc/BDD/EG2.desc
index 98d5e6970..5881d5be7 100644
--- a/regression/ebmc/BDD/EG2.desc
+++ b/regression/ebmc/BDD/EG2.desc
@@ -1,8 +1,8 @@
 CORE
 EG2.smv
 --bdd
-^\[main::spec1\] EG some_var = TRUE: REFUTED$
-^\[main::spec2\] EG some_var = FALSE: REFUTED$
+^\[spec1\] EG some_var = TRUE: REFUTED$
+^\[spec2\] EG some_var = FALSE: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/EX1.desc b/regression/ebmc/BDD/EX1.desc
index 4bd9972a8..ccc4bc52c 100644
--- a/regression/ebmc/BDD/EX1.desc
+++ b/regression/ebmc/BDD/EX1.desc
@@ -1,8 +1,8 @@
 CORE
 EX1.smv
 --bdd
-^\[main::spec1\] EX some_var = TRUE: REFUTED$
-^\[main::spec2\] EX some_var = FALSE: PROVED$
+^\[spec1\] EX some_var = TRUE: REFUTED$
+^\[spec2\] EX some_var = FALSE: PROVED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/EX2.desc b/regression/ebmc/BDD/EX2.desc
index df449e386..ebce097ce 100644
--- a/regression/ebmc/BDD/EX2.desc
+++ b/regression/ebmc/BDD/EX2.desc
@@ -1,8 +1,8 @@
 CORE
 EX2.smv
 --bdd
-^\[main::spec1\] EX some_var = TRUE: REFUTED$
-^\[main::spec2\] EX some_var = FALSE: PROVED$
+^\[spec1\] EX some_var = TRUE: REFUTED$
+^\[spec2\] EX some_var = FALSE: PROVED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/GF1.desc b/regression/ebmc/BDD/GF1.desc
index fe80c7b5f..de4a0ad68 100644
--- a/regression/ebmc/BDD/GF1.desc
+++ b/regression/ebmc/BDD/GF1.desc
@@ -1,7 +1,7 @@
 CORE
 GF1.smv
 --bdd
-^\[main::spec1\] G F some_var: REFUTED$
+^\[spec1\] G F some_var: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/just_p.desc b/regression/ebmc/BDD/just_p.desc
index 670e73cd4..09d5908d4 100644
--- a/regression/ebmc/BDD/just_p.desc
+++ b/regression/ebmc/BDD/just_p.desc
@@ -1,8 +1,8 @@
 CORE
 just_p.smv
 --bdd
-^\[main::spec1\] some_var = TRUE: REFUTED$
-^\[main::spec2\] some_var = FALSE: PROVED$
+^\[spec1\] some_var = TRUE: REFUTED$
+^\[spec2\] some_var = FALSE: PROVED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/Properties1/test.desc b/regression/ebmc/Properties1/test.desc
index 8f4f7f99f..fcfc98022 100644
--- a/regression/ebmc/Properties1/test.desc
+++ b/regression/ebmc/Properties1/test.desc
@@ -1,9 +1,9 @@
 CORE broken-smt-backend
 main.smv
---bound 10 --property main::spec2
+--bound 10 --property spec2
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec2\] .* PROVED up to bound 10$
+^\[spec2\] .* PROVED up to bound 10$
 --
 ^warning: ignoring
-$\[main::spec1\] .*$
+$\[spec1\] .*$
diff --git a/regression/ebmc/elbtunnel/test.desc b/regression/ebmc/elbtunnel/test.desc
index 9e6cde4ce..b9312fbcb 100644
--- a/regression/ebmc/elbtunnel/test.desc
+++ b/regression/ebmc/elbtunnel/test.desc
@@ -3,13 +3,13 @@ elbtunnel.aig.smv
 --bound 12
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] .* REFUTED$
-^\[main::spec2\] .* PROVED up to bound 12$
-^\[main::spec3\] .* REFUTED$
-^\[main::spec4\] .* REFUTED$
-^\[main::spec5\] .* PROVED up to bound 12$
-^\[main::spec6\] .* PROVED up to bound 12$
-^\[main::spec7\] .* REFUTED$
-^\[main::spec8\] .* REFUTED$
+^\[spec1\] .* REFUTED$
+^\[spec2\] .* PROVED up to bound 12$
+^\[spec3\] .* REFUTED$
+^\[spec4\] .* REFUTED$
+^\[spec5\] .* PROVED up to bound 12$
+^\[spec6\] .* PROVED up to bound 12$
+^\[spec7\] .* REFUTED$
+^\[spec8\] .* REFUTED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/range_type/range_type1.desc b/regression/ebmc/range_type/range_type1.desc
index 1bd21a32e..6a72be6c8 100644
--- a/regression/ebmc/range_type/range_type1.desc
+++ b/regression/ebmc/range_type/range_type1.desc
@@ -3,6 +3,6 @@ range_type1.smv
 --bound 10
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec1\] AG x != 4: PROVED up to bound 10$
+^\[spec1\] AG x != 4: PROVED up to bound 10$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/range_type/range_type2.desc b/regression/ebmc/range_type/range_type2.desc
index c4d238377..db50dd468 100644
--- a/regression/ebmc/range_type/range_type2.desc
+++ b/regression/ebmc/range_type/range_type2.desc
@@ -3,7 +3,7 @@ range_type2.smv
 --bound 10
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec1\] AG TRUE: PROVED up to bound 10$
-^\[main::spec2\] AG NET_tmp9: PROVED up to bound 10$
+^\[spec1\] AG TRUE: PROVED up to bound 10$
+^\[spec2\] AG NET_tmp9: PROVED up to bound 10$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/range_type/range_type3.desc b/regression/ebmc/range_type/range_type3.desc
index 0c2362bbe..08f48a437 100644
--- a/regression/ebmc/range_type/range_type3.desc
+++ b/regression/ebmc/range_type/range_type3.desc
@@ -3,7 +3,7 @@ range_type3.smv
 --bound 10 --trace
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] .* REFUTED$
+^\[spec1\] .* REFUTED$
 ^Counterexample:$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/range_type/range_type4.desc b/regression/ebmc/range_type/range_type4.desc
index 49991cb4b..8c4b05d8f 100644
--- a/regression/ebmc/range_type/range_type4.desc
+++ b/regression/ebmc/range_type/range_type4.desc
@@ -3,6 +3,6 @@ range_type4.smv
 --bound 10
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec1\] AG \(!x = 6\): PROVED up to bound 10$
+^\[spec1\] AG \(!x = 6\): PROVED up to bound 10$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/range_type/range_type5.desc b/regression/ebmc/range_type/range_type5.desc
index ef6f95259..c49089296 100644
--- a/regression/ebmc/range_type/range_type5.desc
+++ b/regression/ebmc/range_type/range_type5.desc
@@ -3,6 +3,6 @@ range_type5.smv
 --bound 3
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec1\] AG \(!x = 6\): PROVED up to bound 3$
+^\[spec1\] AG \(!x = 6\): PROVED up to bound 3$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/small-test1/test.desc b/regression/ebmc/small-test1/test.desc
index 01ce9e93b..430372de6 100644
--- a/regression/ebmc/small-test1/test.desc
+++ b/regression/ebmc/small-test1/test.desc
@@ -3,6 +3,6 @@ main.smv
 --bound 10 --trace
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] AG x = 1: REFUTED$
+^\[spec1\] AG x = 1: REFUTED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/small-test2/test.desc b/regression/ebmc/small-test2/test.desc
index 8e84aa5aa..392bf717f 100644
--- a/regression/ebmc/small-test2/test.desc
+++ b/regression/ebmc/small-test2/test.desc
@@ -3,6 +3,6 @@ main.smv
 --bound 2
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] AG z: REFUTED$
+^\[spec1\] AG z: REFUTED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/smv/bdd_unsupported_property.desc b/regression/ebmc/smv/bdd_unsupported_property.desc
index 85624f367..9e0a5508e 100644
--- a/regression/ebmc/smv/bdd_unsupported_property.desc
+++ b/regression/ebmc/smv/bdd_unsupported_property.desc
@@ -3,7 +3,7 @@ bdd_unsupported_property.smv
 --bdd
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] !G x = FALSE: FAILURE: property not supported by BDD engine$
-^\[main::spec2\] G x = FALSE: REFUTED$
+^\[spec1\] !G x = FALSE: FAILURE: property not supported by BDD engine$
+^\[spec2\] G x = FALSE: REFUTED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/smv/bmc_unsupported_property1.desc b/regression/ebmc/smv/bmc_unsupported_property1.desc
index e1b60e7d1..0e6d424c9 100644
--- a/regression/ebmc/smv/bmc_unsupported_property1.desc
+++ b/regression/ebmc/smv/bmc_unsupported_property1.desc
@@ -3,7 +3,7 @@ bmc_unsupported_property1.smv
 
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] EG x = FALSE: FAILURE: property not supported by BMC engine$
-^\[main::spec2\] G x = FALSE: REFUTED$
+^\[spec1\] EG x = FALSE: FAILURE: property not supported by BMC engine$
+^\[spec2\] G x = FALSE: REFUTED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/smv/bmc_unsupported_property2.desc b/regression/ebmc/smv/bmc_unsupported_property2.desc
index b9daf9b57..8680f5235 100644
--- a/regression/ebmc/smv/bmc_unsupported_property2.desc
+++ b/regression/ebmc/smv/bmc_unsupported_property2.desc
@@ -3,7 +3,7 @@ bmc_unsupported_property2.smv
 
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] EG x = FALSE: FAILURE: property not supported by BMC engine$
-^\[main::spec2\] G x = TRUE: PROVED up to bound 1$
+^\[spec1\] EG x = FALSE: FAILURE: property not supported by BMC engine$
+^\[spec2\] G x = TRUE: PROVED up to bound 1$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/smv/bmc_unsupported_property3.desc b/regression/ebmc/smv/bmc_unsupported_property3.desc
index a464d9501..030e6442f 100644
--- a/regression/ebmc/smv/bmc_unsupported_property3.desc
+++ b/regression/ebmc/smv/bmc_unsupported_property3.desc
@@ -3,7 +3,7 @@ bmc_unsupported_property3.smv
 --aig
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] !G x = FALSE: FAILURE: property not supported by netlist BMC engine$
-^\[main::spec2\] G x = FALSE: REFUTED$
+^\[spec1\] !G x = FALSE: FAILURE: property not supported by netlist BMC engine$
+^\[spec2\] G x = FALSE: REFUTED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/smv/initial1.desc b/regression/ebmc/smv/initial1.desc
index e9cd78b86..8e2645bc8 100644
--- a/regression/ebmc/smv/initial1.desc
+++ b/regression/ebmc/smv/initial1.desc
@@ -1,8 +1,8 @@
 CORE
 initial1.smv
 --bound 0
-^\[main::spec1\] tmp1 = TRUE: PROVED up to bound 0$
-^\[main::spec2\] tmp2 = TRUE: REFUTED$
+^\[spec1\] tmp1 = TRUE: PROVED up to bound 0$
+^\[spec2\] tmp2 = TRUE: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/smv/smv1.desc b/regression/ebmc/smv/smv1.desc
index 9ce300840..ae4d345d5 100644
--- a/regression/ebmc/smv/smv1.desc
+++ b/regression/ebmc/smv/smv1.desc
@@ -3,6 +3,6 @@ smv1.smv
 --bdd
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec1\] .* PROVED$
+^\[spec1\] .* PROVED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/smv/smv2.desc b/regression/ebmc/smv/smv2.desc
index f68b1eab4..cc8d2a134 100644
--- a/regression/ebmc/smv/smv2.desc
+++ b/regression/ebmc/smv/smv2.desc
@@ -3,6 +3,6 @@ smv2.smv
 --module main --bound 2 --k-induction
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec1\] .* PROVED$
+^\[spec1\] .* PROVED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/smv/smv3.desc b/regression/ebmc/smv/smv3.desc
index a356a2799..2fb488f79 100644
--- a/regression/ebmc/smv/smv3.desc
+++ b/regression/ebmc/smv/smv3.desc
@@ -3,6 +3,6 @@ smv3.smv
 --module main --bound 2 --k-induction
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec1\] .* PROVED$
+^\[spec1\] .* PROVED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/smv/smv_ltlspec1.desc b/regression/ebmc/smv/smv_ltlspec1.desc
index 05bfdb7a5..146f7f890 100644
--- a/regression/ebmc/smv/smv_ltlspec1.desc
+++ b/regression/ebmc/smv/smv_ltlspec1.desc
@@ -3,6 +3,6 @@ smv_ltlspec1.smv
 --bdd
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec1\] G x != 0: PROVED$
+^\[spec1\] G x != 0: PROVED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/smv/smv_ltlspec2.desc b/regression/ebmc/smv/smv_ltlspec2.desc
index d0880d8e1..4e856ae51 100644
--- a/regression/ebmc/smv/smv_ltlspec2.desc
+++ b/regression/ebmc/smv/smv_ltlspec2.desc
@@ -3,7 +3,7 @@ smv_ltlspec2.smv
 --bdd
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec1\] G F x = 3: PROVED$
+^\[spec1\] G F x = 3: PROVED$
 --
 ^warning: ignoring
 --
diff --git a/regression/ebmc/smv/smv_ltlspec3.desc b/regression/ebmc/smv/smv_ltlspec3.desc
index 6fb16061c..6680836d7 100644
--- a/regression/ebmc/smv/smv_ltlspec3.desc
+++ b/regression/ebmc/smv/smv_ltlspec3.desc
@@ -3,7 +3,7 @@ smv_ltlspec3.smv
 --bound 10 --numbered-trace
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] X X x = TRUE: REFUTED$
+^\[spec1\] X X x = TRUE: REFUTED$
 ^Counterexample with 3 states:$
 ^x@0 = FALSE$
 ^x@1 = FALSE$
diff --git a/regression/ebmc/smv/smv_ltlspec4.desc b/regression/ebmc/smv/smv_ltlspec4.desc
index f96cb0e12..84983b4e0 100644
--- a/regression/ebmc/smv/smv_ltlspec4.desc
+++ b/regression/ebmc/smv/smv_ltlspec4.desc
@@ -3,12 +3,12 @@ smv_ltlspec4.smv
 --bound 10 --numbered-trace
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] F x = 0: REFUTED$
+^\[spec1\] F x = 0: REFUTED$
 ^Counterexample with 3 states:$
 ^x@0 = 1$
 ^x@1 = 2$
 ^x@2 = 2$
-^\[main::spec2\] F x = 2: PROVED up to bound 10$
+^\[spec2\] F x = 2: PROVED up to bound 10$
 --
 ^warning: ignoring
 --
diff --git a/regression/ebmc/traces/numbered1.desc b/regression/ebmc/traces/numbered1.desc
index f2b583d3a..1b464d99e 100644
--- a/regression/ebmc/traces/numbered1.desc
+++ b/regression/ebmc/traces/numbered1.desc
@@ -3,7 +3,7 @@ waveform1.smv
 --bound 20 --numbered-trace
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] .* REFUTED$
+^\[spec1\] .* REFUTED$
 ^Counterexample with 21 states:$
 ^y@0 = 0$
 ^y@10 = 100$
diff --git a/regression/ebmc/traces/waveform1.desc b/regression/ebmc/traces/waveform1.desc
index 51fdb8d59..3fe427b6d 100644
--- a/regression/ebmc/traces/waveform1.desc
+++ b/regression/ebmc/traces/waveform1.desc
@@ -3,7 +3,7 @@ waveform1.smv
 --bound 20 --waveform
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] .* REFUTED$
+^\[spec1\] .* REFUTED$
 ^Counterexample:$
 ^   0  1  2  3  4  5  6  7  8  9  10  11  12  13  14  15  16  17  18  19  20$
 ^x  0  1  2  3  4  5  6  7  8  9  10  11  12  13  14  15  16  17  18  19  20$
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
index 325a4c25d..fa7da4ead 100644
--- a/src/smvlang/smv_typecheck.cpp
+++ b/src/smvlang/smv_typecheck.cpp
@@ -1482,10 +1482,9 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
       {
         symbolt spec_symbol;
 
-        spec_symbol.base_name = smv_module.base_name;
+        spec_symbol.base_name = "spec" + std::to_string(nr++);
         spec_symbol.name =
-          id2string(smv_module.name) + "::spec" + std::to_string(nr++);
-        spec_symbol.pretty_name = strip_smv_prefix(spec_symbol.name);
+          id2string(smv_module.name) + "::" + id2string(spec_symbol.base_name);
         spec_symbol.module = smv_module.name;
         spec_symbol.type = bool_typet();
         spec_symbol.is_property = true;
@@ -1493,6 +1492,11 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
         spec_symbol.value = it->expr;
         spec_symbol.location = it->location;
 
+        if(smv_module.name == "smv::main")
+          spec_symbol.pretty_name = spec_symbol.base_name;
+        else
+          spec_symbol.pretty_name = strip_smv_prefix(spec_symbol.name);
+
         symbol_table.add(spec_symbol);
       }
     }