remove or document unused exception from test.

Author: kfriedberger

src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java

@@ -377,10 +377,8 @@ public BooleanFormula applyTactic(BooleanFormula f, Tactic tactic)
 
   /**
    * Eliminate UFs from the given input formula.
-   *
-   * @throws InterruptedException Can be thrown by the native code.
    */
-  protected BooleanFormula applyUFEImpl(BooleanFormula pF) throws InterruptedException {
+  protected BooleanFormula applyUFEImpl(BooleanFormula pF) {
     return SolverUtils.ufElimination(this).eliminateUfs(pF);
   }
 
@@ -390,6 +388,7 @@ protected BooleanFormula applyUFEImpl(BooleanFormula pF) throws InterruptedExcep
    * <p>This is the light version that does not need to eliminate all quantifiers.
    *
    * @throws InterruptedException Can be thrown by the native code.
+   * @throws SolverException Can be thrown by the native code.
    */
   protected BooleanFormula applyQELightImpl(BooleanFormula pF)
       throws InterruptedException, SolverException {
@@ -404,6 +403,7 @@ protected BooleanFormula applyQELightImpl(BooleanFormula pF)
    *
    * @param pF Input to apply the CNF transformation to.
    * @throws InterruptedException Can be thrown by the native code.
+   * @throws SolverException Can be thrown by the native code.
    */
   protected BooleanFormula applyCNFImpl(BooleanFormula pF)
       throws InterruptedException, SolverException {
@@ -417,6 +417,7 @@ protected BooleanFormula applyCNFImpl(BooleanFormula pF)
    * Apply negation normal form (NNF) transformation to the given input formula.
    *
    * @throws InterruptedException Can be thrown by the native code.
+   * @throws SolverException Can be thrown by the native code.
    */
   protected BooleanFormula applyNNFImpl(BooleanFormula input)
       throws InterruptedException, SolverException {
@@ -434,6 +435,7 @@ public <T extends Formula> T simplify(T f) throws InterruptedException, SolverEx
    * <p>This does not need to change something, but it might simplify the formula.
    *
    * @throws InterruptedException Can be thrown by the native code.
+   * @throws SolverException Can be thrown by the native code.
    */
   protected TFormulaInfo simplify(TFormulaInfo f) throws InterruptedException, SolverException {
     return f;

src/org/sosy_lab/java_smt/test/SolverTacticsTest.java

@@ -199,7 +199,7 @@ public void ufEliminationNestedUfsTest() throws SolverException, InterruptedExce
   }
 
   @Test
-  public void ufEliminationNestedQuantifierTest() throws InterruptedException, SolverException {
+  public void ufEliminationNestedQuantifierTest() {
     requireIntegers();
     requireQuantifiers();
     // f := exists v1,v2v,v3,v4 : uf(v1, v3) == uf(v2, v4)