Consider all non-obvious choose's to be impure

epfl-lara · May 21, 2019 · 08fb4ef · 08fb4ef
1 parent 397ae7b
commit 08fb4ef
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/main/scala/inox/transformers/SimplifierWithPC.scala b/src/main/scala/inox/transformers/SimplifierWithPC.scala
@@ -94,7 +94,7 @@ trait SimplifierWithPC extends Transformer { self =>
     case e if path implies not(e) => (BooleanLiteral(false).copiedFrom(e), true)
 
     case c @ Choose(res, BooleanLiteral(true)) if hasInstance(res.tpe) == Some(true) => (c, true)
-    case c: Choose => (c, opts.assumeChecked)
+    case c: Choose => (c, false)
 
     case Lambda(params, body) =>
       val (rb, _) = simplify(body, path withBounds params)