| 1997 | } |
| 1998 | |
| 1999 | expr expr::toBVBool() const { |
| 2000 | auto sort = mkBVSort(1); |
| 2001 | return mkIf(*this, mkUInt(1, sort), mkUInt(0, sort)); |
| 2002 | } |
| 2003 | |
| 2004 | expr expr::float2BV() const { |
| 2005 | if (auto app = isAppOf(Z3_OP_FPA_TO_FP)) // ((_ to_fp e s) BV) |