Fix stuck CounterExample Dialog

In case of an exception when translating the formula to SMT input, the CE Dialog could not be dismissed, requiring KeY to be restarted.

key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/AbstractCounterExampleGenerator.java

@@ -68,14 +68,12 @@ public void searchCounterExample(UserInterfaceControl ui, Proof oldProof, Sequen
             throw new IllegalStateException(
                 "Can't find SMT solver " + SolverTypes.Z3_CE_SOLVER.getName());
         }
-
         final Proof proof =
             createProof(ui, oldProof, oldSequent, "Semantics Blasting: " + oldProof.name());
         final SemanticsBlastingMacro macro = new SemanticsBlastingMacro();
         TaskFinishedInfo info = ProofMacroFinishedInfo.getDefaultInfo(macro, proof);
         final ProverTaskListener ptl = ui.getProofControl().getDefaultProverTaskListener();
         ptl.taskStarted(new DefaultTaskStartedInfo(TaskKind.Macro, macro.getName(), 0));
-
         try {
             synchronized (macro) { // TODO: Useless? No other thread has access to macro wait for
                                    // macro to terminate
@@ -99,8 +97,6 @@ public void searchCounterExample(UserInterfaceControl ui, Proof oldProof, Sequen
         solvers.add(SolverTypes.Z3_CE_SOLVER);
 
         launcher.launch(solvers, SMTProblem.createSMTProblems(proof), proof.getServices());
-
-
     }
 
     /**

key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java

@@ -255,7 +255,7 @@ public void run() {
         String[] commands;
         try {
             commands = translateToCommand(problem.getSequent());
-        } catch (IllegalFormulaException e) {
+        } catch (Throwable e) {
             interruptionOccurred(e);
             listener.processInterrupted(this, problem, e);
             setSolverState(SolverState.Stopped);

key.core/src/main/java/de/uka/ilkd/key/smt/SolverLauncher.java

@@ -286,15 +286,13 @@ private void launchSolvers(Queue<SMTSolver> solvers, Collection<SMTProblem> prob
         // Launch all solvers until the queue is empty or the launcher is
         // interrupted.
         launchLoop(solvers);
-
         // at this point either there are no solvers left to start or
         // the whole launching process was interrupted.
         waitForRunningSolvers();
 
         cleanUp(solvers);
 
         notifyListenersOfStop();
-
     }
 
     private void notifyListenersOfStart(Collection<SMTProblem> problems,
@@ -320,7 +318,6 @@ private void launchLoop(Queue<SMTSolver> solvers) {
                         // if there is nothing to do, wait for the next solver
                         // finishing its task.
                         wait.await();
-
                     } catch (InterruptedException e) {
                         launcherInterrupted(e);
                     }
@@ -386,8 +383,8 @@ private void notifySolverHasFinished(SMTSolver solver) {
         lock.lock();
         try {
             session.removeCurrentlyRunning(solver);
-            wait.signal();
         } finally {
+            wait.signal();
             lock.unlock();
         }
     }

key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java

@@ -205,7 +205,6 @@ private JButton getStopButton() {
                 if (modus.equals(Modus.SOLVERS_RUNNING)) {
                     listener.stopButtonClicked();
                 }
-
             });
         }
         return stopButton;

keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java

@@ -9,9 +9,7 @@
 import javax.swing.*;
 
 import de.uka.ilkd.key.control.AutoModeListener;
-import de.uka.ilkd.key.control.UserInterfaceControl;
 import de.uka.ilkd.key.core.InterruptListener;
-import de.uka.ilkd.key.core.KeYMediator;
 import de.uka.ilkd.key.core.KeYSelectionEvent;
 import de.uka.ilkd.key.core.KeYSelectionListener;
 import de.uka.ilkd.key.gui.IssueDialog;
@@ -22,8 +20,6 @@
 import de.uka.ilkd.key.logic.Sequent;
 import de.uka.ilkd.key.macros.SemanticsBlastingMacro;
 import de.uka.ilkd.key.proof.*;
-import de.uka.ilkd.key.proof.init.InitConfig;
-import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
 import de.uka.ilkd.key.settings.DefaultSMTSettings;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
 import de.uka.ilkd.key.smt.SolverLauncherListener;
@@ -70,15 +66,12 @@ public void init() {
             @Override
             public void selectedNodeChanged(KeYSelectionEvent e) {
                 final Proof proof = getMediator().getSelectedProof();
-
                 if (proof == null) {
                     // no proof loaded
                     setEnabled(false);
                 } else {
                     final Node selNode = getMediator().getSelectedNode();
                     // Can be applied only to root nodes
-
-
                     setEnabled(haveZ3CE && selNode.childrenCount() == 0 && !selNode.isClosed());
                 }
             }
@@ -102,7 +95,6 @@ public void autoModeStarted(ProofEvent e) {
             @Override
             public void autoModeStopped(ProofEvent e) {
                 getMediator().addKeYSelectionListener(selListener);
-                selListener.selectedNodeChanged(null);
             }
         });
         selListener.selectedNodeChanged(new KeYSelectionEvent(getMediator().getSelectionModel()));
@@ -112,16 +104,16 @@ public void autoModeStopped(ProofEvent e) {
     public void actionPerformed(ActionEvent e) {
         try {
             // Get required information
-            Goal goal = getMediator().getSelectedGoal();
-            Node node = goal.node();
-            Proof oldProof = node.proof();
-            Sequent oldSequent = node.sequent();
-            // Start SwingWorker (CEWorker) in which counter example search is performed.
-            getMediator().stopInterface(true);
-            getMediator().setInteractive(false);
-            CEWorker worker = new CEWorker(oldProof, oldSequent);
-            getMediator().addInterruptedListener(worker);
-            worker.execute();
+            final Goal goal = getMediator().getSelectedGoal();
+            if (goal != null) {
+                final Node node = goal.node();
+                // Start SwingWorker (CEWorker) in which counter example search is performed.
+                getMediator().stopInterface(true);
+                getMediator().setInteractive(false);
+                CEWorker worker = new CEWorker(node.proof(), node.sequent());
+                getMediator().addInterruptedListener(worker);
+                worker.execute();
+            }
         } catch (Exception exc) {
             LOGGER.error("", exc);
             IssueDialog.showExceptionDialog(mainWindow, exc);
@@ -165,74 +157,6 @@ protected SolverLauncherListener createSolverListener(DefaultSMTSettings setting
         }
     }
 
-    /**
-     * Performs the {@link SemanticsBlastingMacro} in a {@link Proof} registered in the
-     * {@link MainWindow} and thus visible to the user. Results are shown with help of the
-     * {@link SolverListener}.
-     * <p>
-     * <b>This class provides only the user interface and no counter example generation logic which
-     * is implemented by the {@link AbstractCounterExampleGenerator}</b>.
-     */
-    public static class MainWindowCounterExampleGenerator extends AbstractCounterExampleGenerator {
-        /**
-         * The {@link KeYMediator} to use.
-         */
-        private final KeYMediator mediator;
-
-        /**
-         * Constructor.
-         *
-         * @param mediator The {@link KeYMediator} to use.
-         */
-        public MainWindowCounterExampleGenerator(KeYMediator mediator) {
-            this.mediator = mediator;
-        }
-
-        /**
-         * {@inheritDoc}
-         */
-        @Override
-        protected Proof createProof(UserInterfaceControl ui, Proof oldProof, Sequent oldSequent,
-                String proofName) {
-            Sequent newSequent = createNewSequent(oldSequent);
-            InitConfig newInitConfig = oldProof.getInitConfig().deepCopy();
-            Proof proof = new Proof(proofName, newSequent, "", newInitConfig.createTacletIndex(),
-                newInitConfig.createBuiltInRuleIndex(), newInitConfig);
-
-            proof.setEnv(oldProof.getEnv());
-            proof.setNamespaces(oldProof.getNamespaces());
-
-            ProofAggregate pa = new SingleProof(proof, "XXX");
-
-            ui.registerProofAggregate(pa);
-
-            SpecificationRepository spec = proof.getServices().getSpecificationRepository();
-            spec.registerProof(spec.getProofOblInput(oldProof), proof);
-
-            mediator.goalChosen(proof.getOpenGoal(proof.root()));
-
-            return proof;
-        }
-
-        /**
-         * {@inheritDoc}
-         */
-        @Override
-        protected void semanticsBlastingCompleted(UserInterfaceControl ui) {
-            mediator.setInteractive(true);
-            mediator.startInterface(true);
-        }
-
-        /**
-         * {@inheritDoc}
-         */
-        @Override
-        protected SolverLauncherListener createSolverListener(DefaultSMTSettings settings,
-                Proof proof) {
-            return new SolverListener(settings, proof);
-        }
-    }
-
     private class CEWorker extends SwingWorker<Void, Void> implements InterruptListener {
         private final Proof oldProof;
         private final Sequent oldSequent;