This class is responsible for invoking the back-end decision procedure CVCLite on a
Benchmark, evaluating its results and returning them represented properly to
DecisionProcedureSmtAuflia author: akuwertz version: 1.0, 05/08/2006
A mere constructor.
Parameters: goal - the Goal which should be checked for satisfiability Parameters: dptf - the DecisionProcedureTranslationFactory used to ranslate the thesequent of the goal Parameters: services - the Services used during the translation process
This method is reponsible executing and evaluating CVCLite. It implements the hook provided in
DecisionProcedureSmtAuflia throws: RuntimeException - if an Exception occured due to the invocation or execution of CVCLite
Methods inherited from de.uka.ilkd.key.proof.decproc.DecisionProcedureSmtAuflia