В настоящее время я использую API Alloy Analyzer для создания программы и получаю некоторые специфические действия. В частности, если я открою файл и проанализирую его (используя CompUtil.parseEverything), затем создаю новую команду и вызываю TranslateAlloyToKodkod.execute_command для проанализированного файла и вновь созданную команду, используя MiniSat с ядром UNSAT, он работает нормально. Однако позже во время выполнения моя программа анализирует второй входной файл (также используя CompUtil.parseEverything), получает другой мир, создает новую команду, а затем я снова пытаюсь вызвать TranslateAlloyToKodkod.execute_command и выдает следующую ошибку:

ERROR: class edu.mit.csail.sdg.alloy4.ErrorFatal: The required JNI library cannot be found: java.lang.UnsatisfiedLinkError: no minisatproverx5 in java.library.path edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod.execute_command(TranslateAlloyToKodkod.java:390)

У кого-нибудь есть идеи, почему это выбрасывается второй раз, а не первый?

Подводя итог, у меня есть нечто похожее на следующее:

Module someWorld = CompUtil.parseEverything_fromFile(rep, null, "someFile.als");
//For the following, "sig" is a sig in someWorld.getAllReachableSigs();
Command command = sig.not();
A4Options options = new A4Options();
options.solver = A4Options.SatSolver.MiniSatProverJNI;
A4Solution ans = 
    TranslateAlloyToKodkod.execute_command(rep, someWorld, command, options);
//No thrown error
Module someOtherWorld = CompUtil.parseEverything_fromFile(rep, null, "someOtherFile.als");
//For the following, "sig" is a sig in someOtherWorld.getAllReachableSigs();
Command commandTwo = sig.not();
A4Solution ansTwo = 
    TranslateAlloyToKodkod.execute_command(rep, someOtherWorld, commandTwo, options);
//Thrown error above. Why?