From ff41b7b93ffbf59b685815b1fc28a7649fa58123 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 20 Apr 2015 17:57:59 +0200
Subject: [PATCH] Make sure we don't crash in case there is no variables
---
.../leon/solvers/smtlib/SMTLIBTarget.scala | 24 +++++++++++--------
1 file changed, 14 insertions(+), 10 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index fd687b778..8d4d7c174 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -702,20 +702,24 @@ trait SMTLIBTarget {
override def getModel: Map[Identifier, Expr] = {
val syms = variables.bSet.toList
- val cmd: Command =
- GetValue(syms.head,
- syms.tail.map(s => QualifiedIdentifier(SMTIdentifier(s)))
- )
+ if (syms.isEmpty) {
+ Map()
+ } else {
+ val cmd: Command =
+ GetValue(syms.head,
+ syms.tail.map(s => QualifiedIdentifier(SMTIdentifier(s)))
+ )
- val GetValueResponseSuccess(valuationPairs) = sendCommand(cmd)
+ val GetValueResponseSuccess(valuationPairs) = sendCommand(cmd)
- valuationPairs.collect {
- case (SimpleSymbol(sym), value) if variables.containsB(sym) =>
- val id = variables.toA(sym)
+ valuationPairs.collect {
+ case (SimpleSymbol(sym), value) if variables.containsB(sym) =>
+ val id = variables.toA(sym)
- (id, fromSMT(value, id.getType)(Map(), Map()))
- }.toMap
+ (id, fromSMT(value, id.getType)(Map(), Map()))
+ }.toMap
+ }
}
override def push(): Unit = {
--
GitLab