Unable to use SAT/SMT features of NuXMV
While there is provision to add infinite state variables like unbounded integers and reals, formal verification doesn’t work for designs since only check_property command is generated and executed using NuSMV/NuXMV. Feature to use other SAT/SMT commands can be added.
(from redmine: issue id 3724, created on 2019-04-28)