[analyzer] Fixed bitvector from model always being unsigned

[mikhail.ramalho]

Summary

Getting an APSInt from the model always returned an unsigned integer because of the unused parameter.

This was not breaking any test case because no code relies on the actual value of the integer returned here, but rather it is only used to check if a symbol has more than one solution in getSymVal.

[george.karpenkov]

Makes sense.

Do you have examples where it makes difference in practice?

[mikhail.ramalho]

It doesn't make any difference in practice, for now.

It should only start to be a problem if people use the counterexample to do fancy stuff (maybe the automatic test generation that Artem mentioned in the mailing list?).

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) override {
     return newExprRef(
         Z3Expr(Context, Z3_mk_const(Context.Context,
                                     Z3_mk_string_symbol(Context.Context, Name),
                                     toZ3Sort(*Sort).Sort)));
   }
 
   llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,
                             bool isUnsigned) override {
-    return llvm::APSInt(llvm::APInt(
-        BitWidth, Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST),
-        10));
+    return llvm::APSInt(
+        llvm::APInt(BitWidth,
+                    Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST),
+                    10),
+        isUnsigned);
   }
 
   bool getBoolean(const SMTExprRef &Exp) override {
     return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE;
   }
 
   SMTExprRef getFloatRoundingMode() override {
     // TODO: Don't assume nearest ties to even rounding mode