Model the llvm.assume intrinsic as a no-op

Currently we don't do anything with LLVM's assume statement. This is because we
need to be sure that the assumption provided to the function is correct. At best
it might help with verification, but it could also lead SMACK to report erroneous
bugs. For now, this removes this intrinsic, preventing a warning about an unsound
call to this function.

Author: keram88

lib/smack/SmackInstGenerator.cpp

@@ -887,6 +887,14 @@ void SmackInstGenerator::generateUnModeledCall(llvm::CallInst *ci) {
 void SmackInstGenerator::visitIntrinsicInst(llvm::IntrinsicInst &ii) {
   processInstruction(ii);
 
+  // The llvm.assume intrinsic currently has no use in SMACK. This is an
+  // optimization hint for LLVM. If we ever want to exploit this function,
+  // we need to make sure that it is used soundly.
+  //
+  // Nothing is done with this to prevent warnings about this intrinsic
+  // being unsoundly modeled.
+  static const auto assume = [this](CallInst *ci) { return; };
+
   //(CallInst -> Void) -> [Flags] -> (CallInst -> Void)
   static const auto conditionalModel =
       [this](std::function<void(CallInst *)> modelGenFunc,
@@ -1132,6 +1140,7 @@ void SmackInstGenerator::visitIntrinsicInst(llvm::IntrinsicInst &ii) {
 
   static const std::map<llvm::Intrinsic::ID, std::function<void(CallInst *)>>
       stmtMap{
+          {llvm::Intrinsic::assume, assume},
           {llvm::Intrinsic::bitreverse, assignBvExpr(bitreverse)},
           {llvm::Intrinsic::bswap, assignBvExpr(bswap)},
           {llvm::Intrinsic::convert_from_fp16, f16UpCast},