FAQ 0001
Q: Can I use nuXmv in a commercial setting?
A: You may study, copy, compile and execute nuXmv only for academic, non-commercial reaserch purposes, subject to the restrictions reported in the LICENSE.txt You may not:

• Modify nuXmv for any purpose.
• Re-distribute nuXmv in any form for any purposes.
  • Examples of purposes would be running business operations, licensing, leasing, or selling the Software, distributing the Software for use with commercial or non-commercial products, using the Software in the creation or use of commercial or non-commercial products. Further details are available in the License page.

FAQ 0002
Q: How can I report a bug about nuXmv?
A: Send an email to

The bug report shall contain:

1. A brief description of the identified problem
2. All needed information to enable us to reproduce it
   • Input files
   • Sequence of commands
3. Any further useful information, e.g. expected behaviour.

FAQ 0003
Q: How can I subscribe/unsubscribe to the nuXmv mailing list?
A: You can subscribe by requesting to join the nuxmv-user group.

FAQ 0004
Q: Can I save a file in SMT-LIB format?
A: The SMT-LIB format is combinational in nature (similarly to a DIMACS file in the pure-boolean case). Thus, you can not save the content of a nuXmv input file (i.e. a transition system plus a set of properties) in SMT-LIB. However, some of the algorithms of nuXmv allow you to save combinational problems that result from the analysis of transition systems (e.g. the unrolling up to a given depth of a bounded model checking problem).