You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The following odd-looking snippet sometimes goes through with --solvers="no-inc:smt-z3:z3 tactic.default_tactic=smt sat.euf=true" (a solver we sometimes use, see e.g. SortedArray) even though it should not:
importstainless.*importstainless.lang.*importstainless.proof.*importstainless.collection.*objectMin {
caseclassWrapper(dummy: BigInt, data: Data)
caseclassData(dummy: BigInt, values: ListMap[Int, Int]) {
require(values.contains(3) && values.contains(4))
}
deftest(w: Wrapper, x: BigInt):Unit= {
require(x >=0)
decreases(x)
if (x ==0) {
w match {
case w@Wrapper(_, _) => check(w.data.values.contains(3))
}
()
} else {
test(w, x -1)
}
}.ensuring(_ =>false)
}
I would have thought this bug was introduced by 9fbc579 but I've tested it against an older commit and it went through as well.
Note that smt-cvc4 and smt-z3 provide a correct counter-example.
The text was updated successfully, but these errors were encountered:
The following odd-looking snippet sometimes goes through with
--solvers="no-inc:smt-z3:z3 tactic.default_tactic=smt sat.euf=true"
(a solver we sometimes use, see e.g.SortedArray
) even though it should not:I would have thought this bug was introduced by 9fbc579 but I've tested it against an older commit and it went through as well.
Note that
smt-cvc4
andsmt-z3
provide a correct counter-example.The text was updated successfully, but these errors were encountered: