[PATCH] D79883: Fix Z3 function calls regarding arithmetic operations

Gabor Marton via Phabricator via llvm-commits llvm-commits at lists.llvm.org
Thu May 14 06:58:59 PDT 2020


This revision was automatically updated to reflect the committed changes.
Closed by commit rG5fc05c376a3c: Fix Z3 function calls regarding arithmetic operations (authored by martong).

Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D79883/new/

https://reviews.llvm.org/D79883

Files:
  llvm/lib/Support/Z3Solver.cpp


Index: llvm/lib/Support/Z3Solver.cpp
===================================================================
--- llvm/lib/Support/Z3Solver.cpp
+++ llvm/lib/Support/Z3Solver.cpp
@@ -516,16 +516,16 @@
     SMTExprRef RoundingMode = getFloatRoundingMode();
     return newExprRef(
         Z3Expr(Context,
-               Z3_mk_fpa_mul(Context.Context, toZ3Expr(*LHS).AST,
-                             toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
+               Z3_mk_fpa_mul(Context.Context, toZ3Expr(*RoundingMode).AST,
+                             toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
   }
 
   SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
     SMTExprRef RoundingMode = getFloatRoundingMode();
     return newExprRef(
         Z3Expr(Context,
-               Z3_mk_fpa_div(Context.Context, toZ3Expr(*LHS).AST,
-                             toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
+               Z3_mk_fpa_div(Context.Context, toZ3Expr(*RoundingMode).AST,
+                             toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
   }
 
   SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
@@ -538,16 +538,16 @@
     SMTExprRef RoundingMode = getFloatRoundingMode();
     return newExprRef(
         Z3Expr(Context,
-               Z3_mk_fpa_add(Context.Context, toZ3Expr(*LHS).AST,
-                             toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
+               Z3_mk_fpa_add(Context.Context, toZ3Expr(*RoundingMode).AST,
+                             toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
   }
 
   SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
     SMTExprRef RoundingMode = getFloatRoundingMode();
     return newExprRef(
         Z3Expr(Context,
-               Z3_mk_fpa_sub(Context.Context, toZ3Expr(*LHS).AST,
-                             toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
+               Z3_mk_fpa_sub(Context.Context, toZ3Expr(*RoundingMode).AST,
+                             toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
   }
 
   SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D79883.263993.patch
Type: text/x-patch
Size: 2168 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20200514/41a1fb1e/attachment.bin>


More information about the llvm-commits mailing list