java.lang.NoSuchMethodError: com.microsoft.z3.Solver.getUnsatCore()[Lcom/microsoft/z3/Expr;

There are no available Samebug tips for this exception. Do you have an idea how to solve this issue? A short tip would help users who saw this issue last week.

  • GitHub comment 3#239203324
    via GitHub by fhowar
    ,
    • java.lang.NoSuchMethodError: com.microsoft.z3.Solver.getUnsatCore()[Lcom/microsoft/z3/Expr; at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverContext.solve(NativeZ3SolverContext.java:102) at gov.nasa.jpf.jdart.constraints.InternalConstraintsTree.findNext(InternalConstraintsTree.java:466) at gov.nasa.jpf.jdart.ConcolicMethodExplorer.hasMoreChoices(ConcolicMethodExplorer.java:206) at gov.nasa.jpf.jdart.ConcolicExplorer.hasMoreChoices(ConcolicExplorer.java:206) at gov.nasa.jpf.jdart.JDartChoiceGenerator.hasMoreChoices(JDartChoiceGenerator.java:64) at gov.nasa.jpf.vm.SystemState.advanceCurCg(SystemState.java:883) at gov.nasa.jpf.vm.SystemState.initializeNextTransition(SystemState.java:745) at gov.nasa.jpf.vm.VM.forward(VM.java:1709) at gov.nasa.jpf.search.Search.forward(Search.java:579) at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79) at gov.nasa.jpf.JPF.run(JPF.java:613) at gov.nasa.jpf.jdart.JDart.run(JDart.java:207) at gov.nasa.jpf.jdart.JDart.start(JDart.java:131) at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:108)
    No Bugmate found.