Skip to content

Commit 1d820ee

Browse files
committed
SMV netlists: use TRUE/FALSE instead of 1/0
NuSMV no longer accepts 1/0 for TRUE/FALSE.
1 parent f20c412 commit 1d820ee

File tree

2 files changed

+3
-3
lines changed

2 files changed

+3
-3
lines changed

regression/ebmc/smv-netlist/s_until1.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ CORE
22
s_until1.sv
33
--smv-netlist
44
^LTLSPEC \(\!node144\) U node151$
5-
^LTLSPEC \(1\) U node158$
5+
^LTLSPEC \(TRUE\) U node158$
66
^EXIT=0$
77
^SIGNAL=0$
88
--

src/trans-netlist/smv_netlist.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -51,12 +51,12 @@ void print_smv(const netlistt &netlist, std::ostream &out, literalt a)
5151
{
5252
if(a == const_literal(false))
5353
{
54-
out << "0";
54+
out << "FALSE";
5555
return;
5656
}
5757
else if(a == const_literal(true))
5858
{
59-
out << "1";
59+
out << "TRUE";
6060
return;
6161
}
6262

0 commit comments

Comments
 (0)