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