From 1f5d2ead9fd4fb0c4690a0eb6a9725ba1f988749 Mon Sep 17 00:00:00 2001
From: Jakub Janaszkiewicz <janaszkiewicz.jakub@gmail.com>
Date: Tue, 28 Feb 2023 02:35:37 +0100
Subject: [PATCH] Fix mod operator

---
 .gitignore                     | 1 +
 native-verifier/src/smt_lib.rs | 4 ++--
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/.gitignore b/.gitignore
index 38d1386d7df..d46597917b7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -10,6 +10,7 @@ callgrind.*
 core
 report.csv
 *.profraw
+.DS_Store
 
 *.lock
 !/Cargo.lock
diff --git a/native-verifier/src/smt_lib.rs b/native-verifier/src/smt_lib.rs
index c1731588ff5..50ff82bacb1 100644
--- a/native-verifier/src/smt_lib.rs
+++ b/native-verifier/src/smt_lib.rs
@@ -432,7 +432,7 @@ impl SMTTranslatable for Expression {
                 ConstantValue::Int(i64) => i64.to_string(),
                 ConstantValue::BigInt(s) => s.clone(),
             },
-            Expression::MagicWand(magic_wand) => unimplemented!("Magic wands"),
+            Expression::MagicWand(_) => unimplemented!("Magic wands are not supported"),
             Expression::PredicateAccessPredicate(_access) => {
                 // TODO: access predicates for predicates
                 warn!("PredicateAccessPredicate not supported");
@@ -534,7 +534,7 @@ impl SMTTranslatable for BinaryOpKind {
             BinaryOpKind::Sub => "-",
             BinaryOpKind::Mul => "*",
             BinaryOpKind::Div => "/",
-            BinaryOpKind::Mod => "%",
+            BinaryOpKind::Mod => "mod",
             BinaryOpKind::And => "and",
             BinaryOpKind::Or => "or",
             BinaryOpKind::Implies => "=>",