From a0d0812b0cf01889c82991e539a08ed4fc5d698a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 12 Sep 2017 13:18:52 +0200
Subject: [PATCH] add alias bv2nat for bv2int to make it easier to interoperate
 #1252

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/bv_decl_plugin.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
index b5c79f662..fcf9a9f8f 100644
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@@ -738,6 +738,7 @@ void bv_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const
         op_names.push_back(builtin_name("ext_rotate_right",OP_EXT_ROTATE_RIGHT));
         op_names.push_back(builtin_name("int2bv",OP_INT2BV));
         op_names.push_back(builtin_name("bv2int",OP_BV2INT));
+        op_names.push_back(builtin_name("bv2nat",OP_BV2INT));
         op_names.push_back(builtin_name("mkbv",OP_MKBV));
     }
 }