Download nuXmv 1.0 User Manual

nuXmv 1.0 User Manual
qe.structural.preassert conjuncts enabled
Environment Variable
This is a Boolean variable that enables the pre-assertion in the SMT solver of all the conjuncts, if any, of the
formula to abstract when the qe.engine is set to structural. By default this variable is set to 0, i.e. the
optimization is disabled.
qe.structural.varsampling enabled
Environment Variable
This is a Boolean variable that enables the variable sampling optimization [CDJR09] while performing the
quantification of the formula to abstract when the qe.engine is set to structural. By default this variable
is set to 1, i.e. the optimization is enabled.
write xmi max word width
Environment Variable
This variable controls the maximum number of bits allowed for the bit vectors when dumping the model in
XMI format with the command write xmi model. The default value is 6.
Remark: Large values may lead to huge times in dumping the XMI format. Indeed, for each value of the
word an XMI state may be created.
c
Copyright 2014
by FBK.
135