1 files changed, 4 insertions, 3 deletions

diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend
index 1dde2333..aa8579b1 100644
--- a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend
@@ -20,6 +20,7 @@ import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration
 import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntLiteral

 import java.util.TreeSet

 import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTRealLiteral

+import java.math.BigDecimal

 

 @Data

 class ValueType {

@@ -124,7 +125,7 @@ class SmtModelInterpretation implements LogicModelInterpretation {
 //      }

 

         override getElements(Type type) {

-                return this.typeInterpretation.getElements(type)
+                return this.typeInterpretation.getElements(type)

         }

         

         override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) {

@@ -171,8 +172,8 @@ class SmtModelInterpretation implements LogicModelInterpretation {
         override getAllRealsInStructure() {

                 val res = new TreeSet

                 for(literal : document.eAllContents.filter(SMTRealLiteral).toIterable) {

-                        res += literal.value

-                        res += -literal.value

+                        res += literal.value.doubleValue

+                        res += -literal.value.doubleValue

                 }

                 res

         }