| 912 | } |
| 913 | |
| 914 | void State::addGuardableUB(expr &&ub) { |
| 915 | if (config::disallow_ub_exploitation) { |
| 916 | if (!ub.isConst()) |
| 917 | domain.undef_vars.insert(undef_vars.begin(), undef_vars.end()); |
| 918 | guardable_ub.add(domain.path && !ub); |
| 919 | } else { |
| 920 | addUB(std::move(ub)); |
| 921 | } |
| 922 | } |
| 923 | |
| 924 | void State::addNoReturn(const expr &cond) { |
| 925 | if (cond.isFalse()) |