diff --git a/demo/AssociativeListReloaded.scala b/demo/AssociativeListReloaded.scala index a301c0ad9dd337742f27cdc85d824fca0a6b5020..927de56369816e058be6a90edfea82522eb79b8a 100644 --- a/demo/AssociativeListReloaded.scala +++ b/demo/AssociativeListReloaded.scala @@ -60,7 +60,7 @@ object AssociativeList { def weird(m : Map[Int,Int], k : Int, v : Int) : Boolean = { !(m(k) == v) || m.isDefinedAt(k) - } //holds + } holds // def prop0(l : List, m : Map[Int,Int]) : Boolean = { // size(l) > 4 && asMap(l) == m diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala index e8eb68bd9bae88f4fe2dc7fc1ec771e08ee543b8..d40e54ed876be6138425bac783cb751d2974fc17 100644 --- a/src/purescala/FairZ3Solver.scala +++ b/src/purescala/FairZ3Solver.scala @@ -504,6 +504,8 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac } } case (Some(true), m) => { // SAT + // println("the model is") + // println(m) validatingStopwatch.start val (trueModel, model) = validateAndDeleteModel(m, toCheckAgainstModels, varsInVC, evaluator) validatingStopwatch.stop diff --git a/src/purescala/Z3ModelReconstruction.scala b/src/purescala/Z3ModelReconstruction.scala index ebf8611495e5e1ffbf4601ccd5a112f2f9a98ed3..557bb0d16dacf1219366bff952c73f1f7ddfa0cf 100644 --- a/src/purescala/Z3ModelReconstruction.scala +++ b/src/purescala/Z3ModelReconstruction.scala @@ -30,7 +30,10 @@ trait Z3ModelReconstruction { case None => None case Some((map, elseValue)) => // assert(elseValue == mapRangeNoneConstructors(vt)()) - val singletons = for ((index, value) <- map if z3.getASTKind(value) != mapRangeNoneConstructors(vt)()) yield { + val singletons = for ((index, value) <- map if (z3.getASTKind(value) match { + case Z3AppAST(someCons, _) if someCons == mapRangeSomeConstructors(vt) => true + case _ => false + })) yield { z3.getASTKind(value) match { case Z3AppAST(someCons, List(arg)) if someCons == mapRangeSomeConstructors(vt) => SingletonMap(fromZ3Formula(index), fromZ3Formula(arg)) case _ => scala.Predef.error("unexpected value in map: " + value)