[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)

Balazs Benics via cfe-commits cfe-commits at lists.llvm.org
Thu Jun 13 07:03:12 PDT 2024


================
@@ -434,6 +447,12 @@ class SMTSolver {
   virtual bool isFPSupported() = 0;
 
   virtual void print(raw_ostream &OS) const = 0;
+
+  /// Sets the requested option.
+  virtual void setBoolParam(StringRef Key, bool Value) = 0;
+  virtual void setUnsignedParam(StringRef Key, unsigned Value) = 0;
+
+  virtual std::unique_ptr<SMTSolverStatistics> getStatistics() const = 0;
----------------
steakhal wrote:

It's not used in this PR, and I find it difficult to add test for.
However, in my next PR it's gonna be [used](https://github.com/llvm/llvm-project/pull/95129/files#diff-7c4020235aab08e99f0a84abd569c43e01e5b0ce6ac2182ef1deda8b487734b5R88).

The dump methods are for just debugging, like for the other APIs. This way they remain consistent.

https://github.com/llvm/llvm-project/pull/95128


More information about the cfe-commits mailing list