it compiles again

KeYProject · Dec 9, 2023 · f4a016f · f4a016f
1 parent 7605611
commit f4a016f
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 8 deletions.
diff --git a/.../org/key_project/key4eclipse/common/ui/counterExample/EclipseCounterExampleGenerator.java b/.../org/key_project/key4eclipse/common/ui/counterExample/EclipseCounterExampleGenerator.java
@@ -82,7 +82,7 @@ protected void handleLauncherStarted(Collection<SMTProblem> smtproblems,
       // Check for warnings
       for (SolverType type : solverTypes) {
          if (type.supportHasBeenChecked() && !type.isSupportedVersion()) {
-            information.add(new InformationMessage(SolverListener.computeSolverTypeWarningTitle(type), SolverListener.computeSolverTypeWarningMessage(type), false));
+            information.add(new InformationMessage("Warning:" + type, SolverListener.computeSolverTypeWarningMessage(type), false));
          }
       }
    }
@@ -112,8 +112,8 @@ protected void showResultDialog() {
       dialog.setHelpAvailable(false);
       // Fill PreferenceManager
       for (InternSMTProblem problem : problems) {
-         if (problem.createInformation()) {
-            information.add(new InformationMessage(SolverListener.createExceptionTitle(problem), problem, true));
+         for(var info : problem.getInformation()) {
+            information.add(new InformationMessage(info.getTitle(), problem, true));
          }
          manager.addToRoot(new SMTProblemPreferenceNode(computeProblemId(problem), 
                                                         computeProblemName(problem), 
@@ -133,7 +133,7 @@ protected void showResultDialog() {
     * @return The computed name.
     */
    public static String computeProblemName(InternSMTProblem problem) {
-      return problem.getProblem().getName() + " (" + problem.getSolver().getType().getName() + ")";
+      return problem.getProblem().getName() + " (" + problem/*weigl: disabled .getSolver().getType().getName()*/ + ")";
    }
 
    /**

diff --git a/...n.ui/src/org/key_project/key4eclipse/common/ui/counterExample/SMTProblemPropertyPage.java b/...n.ui/src/org/key_project/key4eclipse/common/ui/counterExample/SMTProblemPropertyPage.java
@@ -72,6 +72,8 @@ public SMTProblemPropertyPage(InternSMTProblem problem) {
    @Override
    protected Control createContents(Composite parent) {
       TabFolder tabFolder = new TabFolder(parent, SWT.NONE);
+
+      /* weigl: disabled. problem does not offer getSolver()
       if (problem.getSolver().getType() == SolverType.Z3_CE_SOLVER &&
           problem.getSolver().getSocket().getQuery() != null) {
          // Create model
@@ -91,7 +93,7 @@ public void menuAboutToShow(IMenuManager manager) {
          viewer.getControl().setMenu(manager.createContextMenu(viewer.getControl()));
          // Create help tab
          createTextTab(tabFolder, "Help", InformationWindow.CE_HELP);
-      }
+      }*/
       for (Information information : problem.getInformation()) {
          createTextTab(tabFolder, information.getTitle(), information.getContent());
       }

diff --git a/.../key_project/key4eclipse/resources/counterexamples/KeYProjectCounterExampleGenerator.java b/.../key_project/key4eclipse/resources/counterexamples/KeYProjectCounterExampleGenerator.java
@@ -73,13 +73,14 @@ protected void handleLauncherStarted(Collection<SMTProblem> smtproblems,
     protected void handleLauncherStopped(final SolverLauncher launcher, 
                                          final Collection<SMTSolver> finishedSolvers) {
         for (InternSMTProblem problem : problems) {
-            if (problem.getSolver().getType() == SolverType.Z3_CE_SOLVER &&
+            /*weigl: disabled. API. 
+              if (problem.getSolver().getType() == SolverType.Z3_CE_SOLVER &&
                     problem.getSolver().getSocket().getQuery() != null) {
                 Model model = problem.getSolver().getSocket().getQuery().getModel();
                 model.removeUnnecessaryObjects();
                 model.addAliases();
                 keYProjectCounterExamples.add(new KeYProjectCounterExample(computeProblemId(problem), computeProblemName(problem), model));
-            }
+            }*/
         }
     }
 
@@ -89,7 +90,7 @@ protected void handleLauncherStopped(final SolverLauncher launcher,
      * @return The computed name.
      */
     public static String computeProblemName(InternSMTProblem problem) {
-       return problem.getProblem().getName() + " (" + problem.getSolver().getType().getName() + ")";
+       return problem.getProblem().getName() + " (" + problem/*weigl disabled: .getSolver().getType().getName() */ + ")";
     }
 
     /**