From 39e4faa2e4c51c9588df233c795b4e85523879cf Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 30 Aug 2016 11:26:10 +0200
Subject: [PATCH] Added $anyconst support to smt2 back-end

---
 backends/smt2/smt2.cc | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index af048859c..43601cd24 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -403,6 +403,16 @@ struct Smt2Worker
 				return;
 			}
 
+			if (cell->type == "$anyconst")
+			{
+				registers.insert(cell);
+				decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
+						get_id(module), idcounter, get_id(module), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y"))));
+				register_bv(cell->getPort("\\Y"), idcounter++);
+				recursive_cells.erase(cell);
+				return;
+			}
+
 			if (cell->type == "$and") return export_bvop(cell, "(bvand A B)");
 			if (cell->type == "$or") return export_bvop(cell, "(bvor A B)");
 			if (cell->type == "$xor") return export_bvop(cell, "(bvxor A B)");
@@ -677,6 +687,13 @@ struct Smt2Worker
 					trans.push_back(stringf("  (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q"))));
 				}
 
+				if (cell->type == "$anyconst")
+				{
+					std::string expr_d = get_bv(cell->getPort("\\Y"));
+					std::string expr_q = get_bv(cell->getPort("\\Y"), "next_state");
+					trans.push_back(stringf("  (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Y"))));
+				}
+
 				if (cell->type == "$mem")
 				{
 					int arrayid = memarrays.at(cell);
-- 
2.30.2