This class is responsible for invoking the back-end decision procedure CVC3 on a
Benchmark, evaluating its results and returning them represented properly to
DecisionProcedureSmtAuflia
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 CVC3. It implements the hook provided in
DecisionProcedureSmtAuflia throws: RuntimeException - if an Exception occured due to the invocation or execution of CVC3
Methods inherited from de.uka.ilkd.key.proof.decproc.DecisionProcedureSmtAuflia