From bf6ab3fc036bdf09c8cc9527e1bb9ff4a6d7346d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 11 May 2015 17:11:52 -0700
Subject: [PATCH] local state

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/rel/tbv.cpp |  1 +
 src/test/ddnf.cpp   | 15 ++++++++-------
 2 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp
index 577817e69..9c740b726 100644
--- a/src/muz/rel/tbv.cpp
+++ b/src/muz/rel/tbv.cpp
@@ -106,6 +106,7 @@ tbv* tbv_manager::allocate(char const* bv) {
         if (*bv == '0') set(*result, i++, tbit::BIT_0);
         else if (*bv == '1') set(*result, i++, tbit::BIT_1);
         else if (*bv == '*') i++;
+        else if (*bv == 'x') i++;
         else if (i == 0 && (*bv == ' ' || *bv == '\t')) ;
         else break;
         ++bv;
diff --git a/src/test/ddnf.cpp b/src/test/ddnf.cpp
index 5ab395e20..8919c7fe9 100644
--- a/src/test/ddnf.cpp
+++ b/src/test/ddnf.cpp
@@ -93,7 +93,7 @@ datalog::ddnf_core* populate_ddnf(char const* file, ptr_vector<tbv>& tbvs) {
             std::getline(is, line);
             tbv* t = tbvm.allocate(line.c_str());
             ddnf->insert(*t);
-            //tbvm.display(std::cout << line << " ", *t) << "\n";
+            IF_VERBOSE(2, tbvm.display(verbose_stream() << line << " ", *t) << "\n";);
             tbvs.push_back(t);
             if (p > P) {
                 std::cout << "port number " << p << " too big " << P << "\n";
@@ -110,16 +110,17 @@ datalog::ddnf_core* populate_ddnf(char const* file, ptr_vector<tbv>& tbvs) {
 }
 
 
-static void read_args(char ** argv, int argc) {
-    if (argc == 3) {
-        g_file = argv[2];
+static void read_args(char ** argv, int argc, int& i) {
+    if (argc = i + 2) {
+        g_file = argv[i + 1];
+        ++i;
         return;
     }
 
     if (!g_file) {
         std::cout << "Need routing table file as argument. Arguments provided: ";
-        for (int i = 0; i < argc; ++i) {
-            std::cout << argv[i] << " ";
+        for (int j = i; j < argc; ++j) {
+            std::cout << argv[j] << " ";
         }
         std::cout << "\n";
         exit(0);
@@ -128,7 +129,7 @@ static void read_args(char ** argv, int argc) {
 }
 
 void tst_ddnf(char ** argv, int argc, int& i) {
-    read_args(argv, argc);
+    read_args(argv, argc, i);
     ptr_vector<tbv> tbvs;
     datalog::ddnf_core* ddnf = populate_ddnf(g_file, tbvs);
     create_forwarding(g_file, *ddnf, tbvs);