VAMPIRE: post-submission push

17 files changed, 28 insertions, 49 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
index 5c40d767..88e234fc 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
index 2d4d0741..8f9c0397 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
index 4f554956..eb6007ec 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
@@ -10,11 +10,9 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolut
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation;

-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConfirmations;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;

-import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl;

 import com.google.common.base.Objects;

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel;

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation;

@@ -35,12 +33,10 @@ import java.util.List;
 import org.eclipse.emf.common.util.EList;

 import org.eclipse.xtend2.lib.StringConcatenation;

 import org.eclipse.xtext.xbase.lib.CollectionLiterals;

-import org.eclipse.xtext.xbase.lib.Conversions;

 import org.eclipse.xtext.xbase.lib.Exceptions;

 import org.eclipse.xtext.xbase.lib.Extension;

 import org.eclipse.xtext.xbase.lib.Functions.Function1;

 import org.eclipse.xtext.xbase.lib.InputOutput;

-import org.eclipse.xtext.xbase.lib.IterableExtensions;

 import org.eclipse.xtext.xbase.lib.ListExtensions;

 import org.eclipse.xtext.xbase.lib.ObjectExtensions;

 import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;

@@ -183,79 +179,66 @@ public class VampireSolver extends LogicReasoner {
         } else {

           InputOutput.println();

           final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig);

-          final long backTransformationStart = System.currentTimeMillis();

-          final ModelResult logicResult = this.backwardMapper.transformOutput(problem, 

-            vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime);

-          long _currentTimeMillis_1 = System.currentTimeMillis();

-          final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart);

-          final Function1<VLSConfirmations, Boolean> _function_1 = (VLSConfirmations it) -> {

-            Class<? extends VLSConfirmations> _class = it.getClass();

-            return Boolean.valueOf(Objects.equal(_class, VLSFiniteModelImpl.class));

-          };

-          Iterable<VLSConfirmations> model = IterableExtensions.<VLSConfirmations>filter(vampSol.getGeneratedModel().getConfirmations(), _function_1);

           String modOut_1 = "no";

-          final Iterable<VLSConfirmations> _converted_model = (Iterable<VLSConfirmations>)model;

-          int _length = ((Object[])Conversions.unwrapArray(_converted_model, Object.class)).length;

-          boolean _greaterThan = (_length > 0);

-          if (_greaterThan) {

+          boolean _isFiniteModelGenerated = vampSol.isFiniteModelGenerated();

+          if (_isFiniteModelGenerated) {

             modOut_1 = "FiniteModel";

           }

           final String realModOut = modOut_1;

           ModelResult _createModelResult_1 = this.resultFactory.createModelResult();

-          final Procedure1<ModelResult> _function_2 = (ModelResult it) -> {

+          final Procedure1<ModelResult> _function_1 = (ModelResult it) -> {

             it.setProblem(null);

             EList<Object> _representation = it.getRepresentation();

             VampireModel _createVampireModel = this.factory.createVampireModel();

-            final Procedure1<VampireModel> _function_3 = (VampireModel it_1) -> {

+            final Procedure1<VampireModel> _function_2 = (VampireModel it_1) -> {

             };

-            VampireModel _doubleArrow = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_3);

+            VampireModel _doubleArrow = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_2);

             _representation.add(_doubleArrow);

             it.setTrace(it.getTrace());

             Statistics _createStatistics = this.resultFactory.createStatistics();

-            final Procedure1<Statistics> _function_4 = (Statistics it_1) -> {

+            final Procedure1<Statistics> _function_3 = (Statistics it_1) -> {

               it_1.setTransformationTime(((int) transformationTime));

               EList<StatisticEntry> _entries = it_1.getEntries();

               StringStatisticEntry _createStringStatisticEntry = this.resultFactory.createStringStatisticEntry();

-              final Procedure1<StringStatisticEntry> _function_5 = (StringStatisticEntry it_2) -> {

+              final Procedure1<StringStatisticEntry> _function_4 = (StringStatisticEntry it_2) -> {

                 it_2.setName("satOut");

                 it_2.setValue("-");

               };

-              StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_5);

+              StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_4);

               _entries.add(_doubleArrow_1);

               EList<StatisticEntry> _entries_1 = it_1.getEntries();

               StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry();

-              final Procedure1<StringStatisticEntry> _function_6 = (StringStatisticEntry it_2) -> {

+              final Procedure1<StringStatisticEntry> _function_5 = (StringStatisticEntry it_2) -> {

                 it_2.setName("satTime");

                 it_2.setValue("-");

               };

-              StringStatisticEntry _doubleArrow_2 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_6);

+              StringStatisticEntry _doubleArrow_2 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_5);

               _entries_1.add(_doubleArrow_2);

               EList<StatisticEntry> _entries_2 = it_1.getEntries();

               StringStatisticEntry _createStringStatisticEntry_2 = this.resultFactory.createStringStatisticEntry();

-              final Procedure1<StringStatisticEntry> _function_7 = (StringStatisticEntry it_2) -> {

+              final Procedure1<StringStatisticEntry> _function_6 = (StringStatisticEntry it_2) -> {

                 it_2.setName("modOut");

                 it_2.setValue(realModOut);

               };

-              StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_2, _function_7);

+              StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_2, _function_6);

               _entries_2.add(_doubleArrow_3);

               EList<StatisticEntry> _entries_3 = it_1.getEntries();

               StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry();

-              final Procedure1<StringStatisticEntry> _function_8 = (StringStatisticEntry it_2) -> {

+              final Procedure1<StringStatisticEntry> _function_7 = (StringStatisticEntry it_2) -> {

                 it_2.setName("modTime");

                 long _solverTime = vampSol.getSolverTime();

                 it_2.setValue(Double.valueOf((_solverTime / 1000.0)).toString());

               };

-              StringStatisticEntry _doubleArrow_4 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_3, _function_8);

+              StringStatisticEntry _doubleArrow_4 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_3, _function_7);

               _entries_3.add(_doubleArrow_4);

             };

-            Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_4);

+            Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_3);

             it.setStatistics(_doubleArrow_1);

           };

-          return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult_1, _function_2);

+          return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult_1, _function_1);

         }

       }

-      MonitoredVampireSolution _monitoredVampireSolution = new MonitoredVampireSolution((-1), null);

-      return this.backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, _monitoredVampireSolution, forwardTrace, transformationTime);

+      return null;

     } catch (Throwable _e) {

       throw Exceptions.sneakyThrow(_e);

     }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
index 887a3a31..07b7d4c3 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
index b4943b57..04a3303b 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
index e3b29572..dbd48bbb 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
index 50ff7011..4f4710d4 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
index 337edcba..19ff819d 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
index c32ba83f..2774bb57 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
index 75e60f21..9b636247 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
index d69b41ea..739f0cd5 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
index 6b91ff7b..96506230 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
index f23063ea..b7d9060d 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
index 0de59fdb..d8bc6614 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
index 6176aca5..512e8a06 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
index c09d929e..d6c90484 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
@@ -59,9 +59,9 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
     final int GLOBAL_MIN = (config.typeScopes.minNewElements - elemsInIM);

     final int GLOBAL_MAX = (config.typeScopes.maxNewElements - elemsInIM);

     final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList();

-    final boolean consistant = (GLOBAL_MAX > GLOBAL_MIN);

+    final boolean consistant = (GLOBAL_MAX >= GLOBAL_MIN);

     if ((GLOBAL_MIN != ABSOLUTE_MIN)) {

-      this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, consistant);

+      this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, (!consistant));

       if (consistant) {

         for (final VLSConstant i : trace.uniqueInstances) {

           localInstances.add(this.support.duplicate(i));

@@ -72,7 +72,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
       }

     }

     if ((GLOBAL_MAX != ABSOLUTE_MAX)) {

-      this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, (!consistant));

+      this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant);

       if (consistant) {

         this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null);

       } else {

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java
index e9073d82..39773357 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java
@@ -7,12 +7,9 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;
 import com.google.common.base.Objects;

 import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;

 import java.io.BufferedReader;

-import java.io.InputStream;

-import java.io.InputStreamReader;

+import java.io.FileReader;

 import java.util.List;

-import org.eclipse.emf.common.util.EList;

 import org.eclipse.emf.common.util.URI;

-import org.eclipse.emf.ecore.EObject;

 import org.eclipse.xtext.xbase.lib.CollectionLiterals;

 import org.eclipse.xtext.xbase.lib.Conversions;

 import org.eclipse.xtext.xbase.lib.Exceptions;

@@ -67,18 +64,17 @@ public class VampireHandler {
         long _minus_1 = (_currentTimeMillis_1 - startTime);

         solverTime = _minus_1;

       }

-      InputStream _inputStream = p.getInputStream();

-      InputStreamReader _inputStreamReader = new InputStreamReader(_inputStream);

-      final BufferedReader reader = new BufferedReader(_inputStreamReader);

+      FileReader _fileReader = new FileReader(solnLoc);

+      final BufferedReader reader = new BufferedReader(_fileReader);

       final List<String> output = CollectionLiterals.<String>newArrayList();

       String line = "";

       while ((!Objects.equal((line = reader.readLine()), null))) {

-        output.add((line + "\n"));

+        boolean _equals_2 = Objects.equal(line, "Finite Model Found!");

+        if (_equals_2) {

+          return new MonitoredVampireSolution(solverTime, null, true);

+        }

       }

-      workspace.getFile(TEMPNAME).delete();

-      final EList<EObject> root = workspace.<VampireModel>readModel(VampireModel.class, SOLNNAME).eResource().getContents();

-      EObject _get = root.get(0);

-      return new MonitoredVampireSolution(solverTime, ((VampireModel) _get));

+      return new MonitoredVampireSolution(solverTime, null, false);

     } catch (Throwable _e) {

       throw Exceptions.sneakyThrow(_e);

     }