From 1d820ee1a5deabcfca8829b40bbc4041a5453227 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 2 May 2025 15:22:34 -0700 Subject: [PATCH] SMV netlists: use TRUE/FALSE instead of 1/0 NuSMV no longer accepts 1/0 for TRUE/FALSE. --- regression/ebmc/smv-netlist/s_until1.desc | 2 +- src/trans-netlist/smv_netlist.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/regression/ebmc/smv-netlist/s_until1.desc b/regression/ebmc/smv-netlist/s_until1.desc index 4d59d8c20..b491f34dc 100644 --- a/regression/ebmc/smv-netlist/s_until1.desc +++ b/regression/ebmc/smv-netlist/s_until1.desc @@ -2,7 +2,7 @@ CORE s_until1.sv --smv-netlist ^LTLSPEC \(\!node144\) U node151$ -^LTLSPEC \(1\) U node158$ +^LTLSPEC \(TRUE\) U node158$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/src/trans-netlist/smv_netlist.cpp b/src/trans-netlist/smv_netlist.cpp index 134f7b97c..61244e9d0 100644 --- a/src/trans-netlist/smv_netlist.cpp +++ b/src/trans-netlist/smv_netlist.cpp @@ -51,12 +51,12 @@ void print_smv(const netlistt &netlist, std::ostream &out, literalt a) { if(a == const_literal(false)) { - out << "0"; + out << "FALSE"; return; } else if(a == const_literal(true)) { - out << "1"; + out << "TRUE"; return; }