diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala index 51dd63d33adef97224d1269ef0270df0f6a069d7..e6c87698cb9c034f6c28fd2246a4c35e39a21d43 100644 --- a/src/main/scala/leon/purescala/ExprOps.scala +++ b/src/main/scala/leon/purescala/ExprOps.scala @@ -1440,6 +1440,12 @@ object ExprOps { case Minus(Plus(e1, e2), Plus(e3, e4)) if e1 == e4 && e2 == e3 => InfiniteIntegerLiteral(0) case Minus(Plus(e1, e2), Plus(Plus(e3, e4), e5)) if e1 == e4 && e2 == e3 => UMinus(e5) + case StringConcat(StringLiteral(""), a) => a + case StringConcat(a, StringLiteral("")) => a + case StringConcat(StringLiteral(a), StringLiteral(b)) => StringLiteral(a+b) + case StringConcat(StringLiteral(a), StringConcat(StringLiteral(b), c)) => StringConcat(StringLiteral(a+b), c) + case StringConcat(StringConcat(c, StringLiteral(a)), StringLiteral(b)) => StringConcat(c, StringLiteral(a+b)) + case StringConcat(a, StringConcat(b, c)) => StringConcat(StringConcat(a, b), c) //default case e => e }).copiedFrom(expr) diff --git a/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala b/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala index be10ff008610e30e2fc3001764fbd0ecf28733af..c66b1e846d2e055ec494b5937aecc5d6a252a8a8 100644 --- a/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala +++ b/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala @@ -136,7 +136,10 @@ class QuestionBuilder[T <: Expr]( val model = new ModelBuilder model ++= elems val modelResult = model.result() - e.eval(s.term, modelResult).result.map(_._1) + for{x <- e.eval(s.term, modelResult).result + res = x._1 + simp = ExprOps.simplifyArithmetic(res)} + yield simp } /** Returns a list of input/output questions to ask to the user. */