using the cvc5 names

HanielB · Feb 23, 2024 · 3f84d06 · 3f84d06
1 parent c635705
commit 3f84d06
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 19 deletions.
diff --git a/carcara/src/ast/mod.rs b/carcara/src/ast/mod.rs
@@ -432,7 +432,7 @@ pub enum IndexedOperator {
 
 impl_str_conversion_traits!(IndexedOperator {
     BvExtract: "extract",
-    BvBitOf: "bit_of",
+    BvBitOf: "bitOf",
     ZeroExtend: "zero_extend",
     SignExtend: "sign_extend",
     RotateLeft: "rotate_left",
@@ -537,7 +537,7 @@ impl_str_conversion_traits!(Operator {
     BvSLe: "bvsle",
     BvSGt: "bvsgt",
     BvSGe: "bvsge",
-    BvBbTerm: "bbterm",
+    BvBbTerm: "bbT",
 
     RareList: "rare-list",
 });

diff --git a/carcara/src/checker/mod.rs b/carcara/src/checker/mod.rs
@@ -555,23 +555,23 @@ impl<'c> ProofChecker<'c> {
             "la_mult_pos" => extras::la_mult_pos,
             "la_mult_neg" => extras::la_mult_neg,
             "mod_simplify" => extras::mod_simplify,
-            "bitblast_const" => bitvectors::value,
-            "bitblast_var" => bitvectors::var,
-            "bitblast_bvand" => bitvectors::and,
-            "bitblast_bvor" => bitvectors::or,
-            "bitblast_bvxor" => bitvectors::xor,
-            "bitblast_bvxnor" => bitvectors::xnor,
-            "bitblast_bvnot" => bitvectors::not,
-            "bitblast_bvcomp" => bitvectors::comp,
-            "bitblast_bvult" => bitvectors::ult,
-            "bitblast_bvslt" => bitvectors::slt,
-            "bitblast_bvadd" => bitvectors::add,
-            "bitblast_bvmult" => bitvectors::mult,
-            "bitblast_bvneg" => bitvectors::neg,
-            "bitblast_equal" => bitvectors::equality,
-            "bitblast_extract" => bitvectors::extract,
-            "bitblast_concat" => bitvectors::concat,
-            "bitblast_sign_extend" => bitvectors::sign_extend,
+            "bv_bitblast_step_const" => bitvectors::value,
+            "bv_bitblast_step_var" => bitvectors::var,
+            "bv_bitblast_step_bvand" => bitvectors::and,
+            "bv_bitblast_step_bvor" => bitvectors::or,
+            "bv_bitblast_step_bvxor" => bitvectors::xor,
+            "bv_bitblast_step_bvxnor" => bitvectors::xnor,
+            "bv_bitblast_step_bvnot" => bitvectors::not,
+            "bv_bitblast_step_bvcomp" => bitvectors::comp,
+            "bv_bitblast_step_bvult" => bitvectors::ult,
+            "bv_bitblast_step_bvslt" => bitvectors::slt,
+            "bv_bitblast_step_bvadd" => bitvectors::add,
+            "bv_bitblast_step_bvmult" => bitvectors::mult,
+            "bv_bitblast_step_bvneg" => bitvectors::neg,
+            "bv_bitblast_step_bvequal" => bitvectors::equality,
+            "bv_bitblast_step_extract" => bitvectors::extract,
+            "bv_bitblast_step_concat" => bitvectors::concat,
+            "bv_bitblast_step_sign_extend" => bitvectors::sign_extend,
 
             "concat_eq" => strings::concat_eq,
             "concat_unify" => strings::concat_unify,