diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala index 93c8c6d021233a6c5968d7de9a78b7c3d135ced1..26f976c095489f22cbc97dd9ee810d1d71ef9f99 100644 --- a/src/main/scala/leon/codegen/CompilationUnit.scala +++ b/src/main/scala/leon/codegen/CompilationUnit.scala @@ -177,6 +177,9 @@ class CompilationUnit(val ctx: LeonContext, case FractionalLiteral(n, d) => new runtime.Rational(n.toString, d.toString) + + case StringLiteral(v) => + new java.lang.String(v) case GenericValue(tp, id) => e diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala index 8b4846a3394c3c3ddd2326d24d23ce95e68f6b05..b82dc6a0f256fec3c3cf733addad76f899456f4a 100644 --- a/src/main/scala/leon/datagen/VanuatooDataGen.scala +++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala @@ -58,6 +58,8 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator { def stringConstructor(s: String) = strings(s) + lazy val stubValues = ints.values ++ bigInts.values ++ booleans.values ++ chars.values ++ rationals.values ++ strings.values + def cPattern(c: Constructor[Expr, TypeTree], args: Seq[VPattern[Expr, TypeTree]]) = { ConstructorPattern[Expr, TypeTree](c, args) } @@ -307,7 +309,6 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator { None }) - val stubValues = ints.values ++ bigInts.values ++ booleans.values ++ chars.values ++ rationals.values val gen = new StubGenerator[Expr, TypeTree](stubValues.toSeq, Some(getConstructors _), treatEmptyStubsAsChildless = true) diff --git a/src/test/scala/leon/integration/solvers/SolversSuite.scala b/src/test/scala/leon/integration/solvers/SolversSuite.scala index 24ebf35916d9abce077fdd7d8ee5752fd3c1e0d3..d568e471f08eb4cf1a558675419daabd9e9c940a 100644 --- a/src/test/scala/leon/integration/solvers/SolversSuite.scala +++ b/src/test/scala/leon/integration/solvers/SolversSuite.scala @@ -72,13 +72,13 @@ class SolversSuite extends LeonTestSuiteWithProgram { val model = solver.getModel for (v <- vs) { if (model.isDefinedAt(v.id)) { - assert(model(v.id).getType === v.getType, "Extracting value of type "+v.getType) + assert(model(v.id).getType === v.getType, s"Solver $solver - Extracting value of type "+v.getType) } else { - fail("Model does not contain "+v.id+" of type "+v.getType) + fail(s"Solver $solver - Model does not contain "+v.id.uniqueName+" of type "+v.getType) } } case _ => - fail("Constraint "+cnstr.asString+" is unsat!?") + fail(s"Solver $solver - Constraint "+cnstr.asString+" is unsat!?") } } finally { solver.free()