Fix mod operator

viperproject · Feb 28, 2023 · 1f5d2ea · 1f5d2ea
1 parent b09e7ab
commit 1f5d2ea
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git 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
@@ -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 => "=>",