delcypher added inline comments.
================ Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:619 + + llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), true); + Z3Expr Z3Int = Z3Expr::fromAPSInt(Int); ---------------- @ddcc Why use APSInt here? Why not APInt, we are looking at raw bits and don't want to interpret the most significant bit in a special way. ================ Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:668 + default: + llvm_unreachable("Unsupported sort to integer!"); + case Z3_BV_SORT: { ---------------- Is `Z3_FLOATING_POINT_SORT` possible in your implementation? https://reviews.llvm.org/D28952 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits