726   SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) override {  in mkBitvector()  argument
730     if (LLVM_UNLIKELY(Int.getBitWidth() > 64u)) {  in mkBitvector()
732       Int.toString(Buffer, 10);  in mkBitvector()
737     const int64_t BitReprAsSigned = Int.getExtValue();  in mkBitvector()
742         Int.isSigned()  in mkBitvector()
752     llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), false);  in mkFloat()  local
753     SMTExprRef Z3Int = mkBitvector(Int, Int.getBitWidth());  in mkFloat()
788     llvm::APSInt Int(Sort->getFloatSortSize(), true);  in toAPFloat()  local
792     if (!toAPSInt(BVSort, AST, Int, true)) {  in toAPFloat()
801     Float = llvm::APFloat(Semantics, Int);  in toAPFloat()
806                 llvm::APSInt &Int, bool useSemantics) {  in toAPSInt()  argument
808       if (useSemantics && Int.getBitWidth() != Sort->getBitvectorSortSize()) {  in toAPSInt()
821         Int = getBitvector(AST, Int.getBitWidth(), Int.isUnsigned());  in toAPSInt()
830       if (useSemantics && Int.getBitWidth() < 1) {  in toAPSInt()
835       Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), getBoolean(AST)),  in toAPSInt()
836                          Int.isUnsigned());  in toAPSInt()
843   bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) override {  in getInterpretation()  argument
854     return toAPSInt(Sort, Assign, Int, true);  in getInterpretation()