From 2114ca25e2525b11e1210534d6752631a958c800 Mon Sep 17 00:00:00 2001 From: Jakub Janaszkiewicz Date: Tue, 28 Feb 2023 02:35:37 +0100 Subject: [PATCH] Fix mod operator --- native-verifier/src/smt_lib.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 => "=>",