SMV netlists: use TRUE/FALSE instead of 1/0

kroening · kroening · commit 44454a4c2785 · 2025-05-02T15:22:34.000-07:00
NuSMV no longer accepts 1/0 for TRUE/FALSE.
diff --git 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;
   }
 

Original file line number	Diff line number	Diff line change
`@@ -51,12 +51,12 @@ void print_smv(const netlistt &netlist, std::ostream &out, literalt a)`
`51`	`51`	`{`
`52`	`52`	`if(a == const_literal(false))`
`53`	`53`	`{`
`54`		`- out << "0";`
	`54`	`+ out << "FALSE";`
`55`	`55`	`return;`
`56`	`56`	`}`
`57`	`57`	`else if(a == const_literal(true))`
`58`	`58`	`{`
`59`		`- out << "1";`
	`59`	`+ out << "TRUE";`
`60`	`60`	`return;`
`61`	`61`	`}`
`62`	`62`