diff options
author | OszkarSemerath <oszkar.semerath@gmail.com> | 2018-03-07 12:48:01 -0500 |
---|---|---|
committer | OszkarSemerath <oszkar.semerath@gmail.com> | 2018-03-07 12:48:01 -0500 |
commit | 5ac36bba74bcf71224d4895cccdae253b07ccbc9 (patch) | |
tree | 85a15ac3d720c24021c9126dc6e00e653135a9b5 /Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend | |
parent | removed unnecessary println (diff) | |
download | VIATRA-Generator-5ac36bba74bcf71224d4895cccdae253b07ccbc9.tar.gz VIATRA-Generator-5ac36bba74bcf71224d4895cccdae253b07ccbc9.tar.zst VIATRA-Generator-5ac36bba74bcf71224d4895cccdae253b07ccbc9.zip |
Rebooting Z3 solver Containment vs Inheritance still has a bug
Diffstat (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend')
-rw-r--r-- | Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend index 4e2e1890..76b1ddbd 100644 --- a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend | |||
@@ -35,8 +35,7 @@ class SMTSolver extends LogicReasoner{ | |||
35 | handler.callSolver(input,configuration) | 35 | handler.callSolver(input,configuration) |
36 | val solverTime = System.currentTimeMillis - solverTimeStart | 36 | val solverTime = System.currentTimeMillis - solverTimeStart |
37 | val outputModel = workspace.reloadModel(typeof(SMTDocument), "problem.smt2") | 37 | val outputModel = workspace.reloadModel(typeof(SMTDocument), "problem.smt2") |
38 | EcoreUtil.resolveAll(outputModel) | 38 | EcoreUtil.resolveAll(outputModel.eResource) |
39 | workspace.deactivateModel("problem.smt2") | ||
40 | return backMapper.transformOutput(problem,outputModel.output,trace, transformationTime, solverTime) | 39 | return backMapper.transformOutput(problem,outputModel.output,trace, transformationTime, solverTime) |
41 | } else throw new IllegalArgumentException('''The configuration have to be an «SmtSolverConfiguration.simpleName»!''') | 40 | } else throw new IllegalArgumentException('''The configuration have to be an «SmtSolverConfiguration.simpleName»!''') |
42 | } | 41 | } |