CVC3 is as its predecessor CVC3 an SMT prover. This rule allows its invocation
from within KeY using the SMT-LIb interface.
See Also:AbstractIntegerRule
A mere constructor.
Parameters: resultWindow - a boolean indicating if the results of this Ruleshould be presented in a separate window Parameters: dptf - the DecisionProcedureTranslationFactory to be used
A mere constructor for convenience. Creates an CVC3IntegerRule with
resultWindow set to true Parameters: dptf - the DecisionProcedureTranslationFactory to be used