I just install NuXMV and want to use it to do Bounded Model Checking. But in user-mannual, the writer says NuXMV doesn't contain Zchaff of minisat. So do i need to install them before starting the work
I use "msat_check_ltlspec_bmc" to verify a simple specification and it can work, and this make me more confused.Here is my simple model.the simple smv model Here is the result.the result
