================
@@ -1059,9 +1066,16 @@ void Environment::assume(const Formula &F) {
DACtx->addFlowConditionConstraint(FlowConditionToken, F);
}
+#if 0
bool Environment::proves(const Formula &F) const {
return DACtx->flowConditionImplies(FlowConditionToken, F);
}
+#else
+bool Environment::proves(const Formula &F) const {
+ auto V = simple_bool_model::getLiteralValue(F, *this);
+ return V.has_value() && *V;
+}
+#endif
bool Environment::allows(const Formula &F) const {
return DACtx->flowConditionAllows(FlowConditionToken, F);
----------------
martinboehme wrote:
Wouldn't this also need to be changed? I _think_ this can just do `return
proves(F);`?
https://github.com/llvm/llvm-project/pull/82950
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
