From 75d7ce2c1dce18ec3c27bfb53ff79e5536fdf2fa Mon Sep 17 00:00:00 2001
From: polgreen <polgreen@amazon.com>
Date: Thu, 19 Oct 2017 19:09:01 +0200
Subject: [PATCH 01/12] Add eager infeasbility, dfs and bfs to symex help file

---
 src/symex/symex_parse_options.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index d28b638..7be39cf 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -636,6 +636,9 @@ void symex_parse_optionst::help()
     " --context-bound nr           limit number of context switches\n"
     " --branch-bound nr            limit number of branches taken\n"
     " --max-search-time s          limit search to approximately s seconds\n"
+    " --dfs                        use depth first search\n"
+    " --bfs                        use breadth first search\n"
+    " --eager-infeasibility        query solver early to determine whether a path is infeasible before searching it\n" // NOLINT(*)
     "\n"
     "Other options:\n"
     " --version                    show version and exit\n"

From c4570187b313614be13db07de2c5f07359501588 Mon Sep 17 00:00:00 2001
From: polgreen <polgreen@amazon.com>
Date: Thu, 19 Oct 2017 15:12:56 +0200
Subject: [PATCH 02/12] Introduce randomized DFS

Randomized DFS shuffles the queue of successor states
---
 src/symex/path_search.cpp         | 25 +++++++++++++++++++++++++
 src/symex/path_search.h           |  8 ++++++--
 src/symex/symex_parse_options.cpp |  8 +++++++-
 src/symex/symex_parse_options.h   |  1 +
 4 files changed, 39 insertions(+), 3 deletions(-)

diff --git a/src/symex/path_search.cpp b/src/symex/path_search.cpp
index 18106ae..9ca139b 100644
--- a/src/symex/path_search.cpp
+++ b/src/symex/path_search.cpp
@@ -20,6 +20,27 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <path-symex/path_symex.h>
 #include <path-symex/build_goto_trace.h>
 
+#include <random>
+
+void path_searcht::shuffle_queue(queuet &queue)
+{
+  if(queue.size()<=1)
+    return;
+
+  INVARIANT(queue.size()<std::numeric_limits<int>::max(),
+      "Queue size must be less than maximum integer");
+  // pick random state and move to front
+  int rand_i = rand() % queue.size();
+
+  std::list<statet>::iterator it = queue.begin();
+  for(int i=0; i<rand_i; i++)
+    it++;
+
+  statet tmp = *it;
+  queue.push_front(tmp);
+  queue.erase(it);
+}
+
 path_searcht::resultt path_searcht::operator()(
   const goto_functionst &goto_functions)
 {
@@ -142,6 +163,9 @@ path_searcht::resultt path_searcht::operator()(
       // execute
       path_symex(state, tmp_queue);
 
+      if(search_heuristic == search_heuristict::RAN_DFS)
+        shuffle_queue(tmp_queue);
+
       // put at head of main queue
       queue.splice(queue.begin(), tmp_queue);
     }
@@ -208,6 +232,7 @@ void path_searcht::pick_state()
   switch(search_heuristic)
   {
   case search_heuristict::DFS:
+  case search_heuristict::RAN_DFS:
     // Picking the first one (most recently added) is a DFS.
     return;
 
diff --git a/src/symex/path_search.h b/src/symex/path_search.h
index 9920723..aa3a39d 100644
--- a/src/symex/path_search.h
+++ b/src/symex/path_search.h
@@ -107,6 +107,7 @@ class path_searcht:public safety_checkert
   };
 
   void set_dfs() { search_heuristic=search_heuristict::DFS; }
+  void set_randomized_dfs() { search_heuristic=search_heuristict::RAN_DFS; }
   void set_bfs() { search_heuristic=search_heuristict::BFS; }
   void set_locs() { search_heuristic=search_heuristict::LOCS; }
 
@@ -120,7 +121,9 @@ class path_searcht:public safety_checkert
   // The states most recently executed are at the head.
   typedef std::list<statet> queuet;
   queuet queue;
-
+  /// Pick random element of queue and move to front
+  /// \param queue  queue to be shuffled
+  void shuffle_queue(queuet &queue);
   // search heuristic
   void pick_state();
 
@@ -151,7 +154,8 @@ class path_searcht:public safety_checkert
   unsigned unwind_limit;
   unsigned time_limit;
 
-  enum class search_heuristict { DFS, BFS, LOCS } search_heuristic;
+  enum class search_heuristict
+  { DFS, RAN_DFS, BFS, LOCS } search_heuristic;
 
   source_locationt last_source_location;
 };
diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index 7be39cf..b2a7243 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -232,7 +232,12 @@ int symex_parse_optionst::doit()
         safe_string2unsigned(cmdline.get_value("max-search-time")));
 
     if(cmdline.isset("dfs"))
-      path_search.set_dfs();
+    {
+      if(cmdline.isset("randomize"))
+        path_search.set_randomized_dfs();
+      else
+        path_search.set_dfs();
+    }
 
     if(cmdline.isset("bfs"))
       path_search.set_bfs();
@@ -638,6 +643,7 @@ void symex_parse_optionst::help()
     " --max-search-time s          limit search to approximately s seconds\n"
     " --dfs                        use depth first search\n"
     " --bfs                        use breadth first search\n"
+    " --randomize                  used in conjunction with dfs, to search by randomized dfs\n" // NOLINT(*)
     " --eager-infeasibility        query solver early to determine whether a path is infeasible before searching it\n" // NOLINT(*)
     "\n"
     "Other options:\n"
diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h
index 99fd3f6..066b83e 100644
--- a/src/symex/symex_parse_options.h
+++ b/src/symex/symex_parse_options.h
@@ -41,6 +41,7 @@ class optionst;
   "(error-label):(verbosity):(no-library)" \
   "(version)" \
   "(bfs)(dfs)(locs)" \
+  "(randomize)" \
   "(cover):" \
   "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \
   "(ppc-macos)(unsigned-char)" \

From 484b21e1886b398d619ec5229e6ab06acc74c3e4 Mon Sep 17 00:00:00 2001
From: polgreen <polgreen@amazon.com>
Date: Sat, 21 Oct 2017 10:37:25 +0200
Subject: [PATCH 03/12] Add distances to property as variable in locst

Also fixes indentation and whitespace in the output function, and replaces unsigned with std::size_t, based on feedback from tautschn
---
 src/path-symex/locs.cpp | 14 +++++++++-----
 src/path-symex/locs.h   |  3 ++-
 2 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/src/path-symex/locs.cpp b/src/path-symex/locs.cpp
index 8f6dd19..ef1026f 100644
--- a/src/path-symex/locs.cpp
+++ b/src/path-symex/locs.cpp
@@ -86,19 +86,23 @@ void locst::output(std::ostream &out) const
 {
   irep_idt function;
 
-  for(unsigned l=0; l<loc_vector.size(); l++)
+  for(std::size_t l = 0; l < loc_vector.size(); l++)
   {
-    const loct &loc=loc_vector[l];
-    if(function!=loc.function)
+    const loct &loc = loc_vector[l];
+    if(function != loc.function)
     {
-      function=loc.function;
+      function = loc.function;
       out << "*** " << function << "\n";
     }
 
     out << "  L" << l << ": "
 //        << loc.target->type << " "
 //        << loc.target->location
-        << " " << as_string(ns, *loc.target) << "\n";
+        << " " << as_string(ns, *loc.target);
+    if(loc_vector[l].distance_to_property
+        != std::numeric_limits<std::size_t>::max())
+      out << " path length: " << loc_vector[l].distance_to_property;
+    out << "\n";
 
     if(!loc.branch_target.is_nil())
       out << "    T: " << loc.branch_target << "\n";
diff --git a/src/path-symex/locs.h b/src/path-symex/locs.h
index a7f54c9..c3578c2 100644
--- a/src/path-symex/locs.h
+++ b/src/path-symex/locs.h
@@ -27,11 +27,12 @@ struct loct
     target(_target),
     function(_function)
   {
+    distance_to_property=std::numeric_limits<std::size_t>::max();
   }
 
   goto_programt::const_targett target;
   irep_idt function;
-
+  std::size_t distance_to_property;
   // we only support a single branch target
   loc_reft branch_target;
 };

From 55d047b1575155cd0f4098d14c21539eb6e01a23 Mon Sep 17 00:00:00 2001
From: polgreen <polgreen@amazon.com>
Date: Sat, 21 Oct 2017 10:43:06 +0200
Subject: [PATCH 04/12] Shortest path grapht

Builds CFG of all program locations and computes the shortest distance from all locations in the graph to a single property.
WARNING: if more than one property is given, we use the first one only.

Writes these distances to the corresponding node in a locs structure passed as argument to the constructor, in order for this to be used to guide the symex search
---
 src/symex/Makefile                |  1 +
 src/symex/shortest_path_graph.cpp | 88 +++++++++++++++++++++++++++++++
 src/symex/shortest_path_graph.h   | 72 +++++++++++++++++++++++++
 3 files changed, 161 insertions(+)
 create mode 100644 src/symex/shortest_path_graph.cpp
 create mode 100644 src/symex/shortest_path_graph.h

diff --git a/src/symex/Makefile b/src/symex/Makefile
index b14e327..3c94eee 100644
--- a/src/symex/Makefile
+++ b/src/symex/Makefile
@@ -2,6 +2,7 @@ SRC = path_search.cpp \
       symex_cover.cpp \
       symex_main.cpp \
       symex_parse_options.cpp \
+      shortest_path_graph.cpp \
       # Empty last line
 
 OBJ += ../../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
diff --git a/src/symex/shortest_path_graph.cpp b/src/symex/shortest_path_graph.cpp
new file mode 100644
index 0000000..e9a416d
--- /dev/null
+++ b/src/symex/shortest_path_graph.cpp
@@ -0,0 +1,88 @@
+/*******************************************************************\
+
+Module: Shortest path graph
+
+Author: elizabeth.polgreen@cs.ox.ac.uk
+
+\*******************************************************************/
+
+#include "shortest_path_graph.h"
+
+#include <algorithm>
+void shortest_path_grapht::bfs(node_indext property_index)
+{
+  // does BFS, not Dijkstra
+  // we hope the graph is sparse
+  std::vector<node_indext> frontier_set;
+
+  frontier_set.reserve(nodes.size());
+
+  frontier_set.push_back(property_index);
+  nodes[property_index].visited = true;
+
+  for(std::size_t d = 1; !frontier_set.empty(); ++d)
+  {
+    std::vector<node_indext> new_frontier_set;
+
+    for(const auto &node_index : frontier_set)
+    {
+      const nodet &n = nodes[node_index];
+
+      // do all neighbors
+      // we go backwards through the graph
+      for(const auto &edge_in : n.in)
+      {
+        node_indext node_in = edge_in.first;
+
+        if(!nodes[node_in].visited)
+        {
+          nodes[node_in].shortest_path_to_property = d;
+          nodes[node_in].visited = true;
+          new_frontier_set.push_back(node_in);
+        }
+      }
+    }
+
+    frontier_set.swap(new_frontier_set);
+  }
+}
+
+void shortest_path_grapht::write_lengths_to_locs()
+{
+  for(const auto &n : nodes)
+  {
+    loc_reft l = target_to_loc_map[n.PC];
+    locs.loc_vector[l.loc_number].distance_to_property
+        = n.shortest_path_to_property;
+  }
+}
+
+void shortest_path_grapht::get_path_lengths_to_property()
+{
+  node_indext property_index;
+  bool found_property=false;
+  for(node_indext n=0; n<nodes.size(); n++)
+  {
+    if(nodes[n].PC->is_assert())
+    {
+      if(found_property == false)
+      {
+        nodes[n].is_property = true;
+        nodes[n].shortest_path_to_property = 0;
+        working_set.insert(n);
+        property_index = n;
+        found_property = true;
+      }
+      else
+        throw "shortest path search cannot be used for multiple properties";
+    }
+  }
+  if(!found_property)
+    throw "unable to find property";
+
+  bfs(property_index);
+
+  write_lengths_to_locs();
+}
+
+
diff --git a/src/symex/shortest_path_graph.h b/src/symex/shortest_path_graph.h
new file mode 100644
index 0000000..813540b
--- /dev/null
+++ b/src/symex/shortest_path_graph.h
@@ -0,0 +1,72 @@
+/*******************************************************************\
+
+Module: Shortest path graph
+
+Author: elizabeth.polgreen@cs.ox.ac.uk
+
+\*******************************************************************/
+
+#ifndef CPROVER_SYMEX_SHORTEST_PATH_GRAPH_H
+#define CPROVER_SYMEX_SHORTEST_PATH_GRAPH_H
+
+#include <goto-programs/cfg.h>
+#include <path-symex/locs.h>
+#include <goto-programs/goto_model.h>
+#include <limits>
+
+
+struct shortest_path_nodet
+{
+  bool visited;
+  std::size_t shortest_path_to_property;
+  bool is_property;
+  shortest_path_nodet():
+    visited(false),
+    is_property(false)
+  {
+    shortest_path_to_property = std::numeric_limits<std::size_t>::max();
+  }
+};
+
+/// \brief constructs a CFG of all program locations. Then computes
+/// the shortest path from every program location to a single property.
+/// WARNING: if more than one property is present in the graph, we will
+/// use the first property found
+/// The distances computed for each node are written to the corresponding
+/// loct in the locst passed as param to the constructor. This allows us
+/// to use these numbers to guide a symex search
+/// \param goto functions to create the CFG from, locs struct made from the
+/// same goto_functions
+class shortest_path_grapht: public cfg_baset<shortest_path_nodet>
+{
+public:
+  explicit shortest_path_grapht(
+      const goto_functionst &_goto_functions, locst &_locs):
+    locs(_locs),
+    target_to_loc_map(_locs)
+    {
+    cfg_baset<shortest_path_nodet>::operator()(_goto_functions);
+    get_path_lengths_to_property();
+    }
+
+protected:
+  /// \brief writes the computed shortest path for every node
+  /// in the graph to the corresponding location in locst.
+  /// This is done so that we can use these numbers to guide
+  /// a search heuristic for symex
+  void write_lengths_to_locs();
+  /// \brief computes the shortest path from every node in
+  /// the graph to a single property. WARNING: if more than one property
+  /// is present, we use the first one discovered.
+  /// Calls bfs() to do this.
+  void get_path_lengths_to_property();
+  /// \brief implements backwards BFS to compute distance from every node in
+  /// the graph to the node index given as parameter
+  /// \param destination node index
+  void bfs(node_indext property_index);
+  std::set<node_indext> working_set;
+  locst &locs;
+  target_to_loc_mapt target_to_loc_map;
+};
+
+#endif /* CPROVER_SYMEX_SHORTEST_PATH_GRAPH_H */

From f67f64e2987dce68e15df97fc3aa0ae84dae9c4a Mon Sep 17 00:00:00 2001
From: polgreen <polgreen@amazon.com>
Date: Sat, 21 Oct 2017 10:46:16 +0200
Subject: [PATCH 05/12] Per function shortest path graph

Builds a CFG for every goto_program in goto_functions, and computes the distance for every location in the CFGs to the property, if one exists in taht CFG, or to the end of the function

Writes these numbers to locst passed as argument to the constructor, in order to use numbers to guide symex search
---
 src/symex/shortest_path_graph.cpp | 50 +++++++++++++++++++++++++++++++
 src/symex/shortest_path_graph.h   | 37 +++++++++++++++++++++++
 2 files changed, 87 insertions(+)

diff --git a/src/symex/shortest_path_graph.cpp b/src/symex/shortest_path_graph.cpp
index e9a416d..b1b6977 100644
--- a/src/symex/shortest_path_graph.cpp
+++ b/src/symex/shortest_path_graph.cpp
@@ -9,6 +9,56 @@ Author: elizabeth.polgreen@cs.ox.ac.uk
 #include "shortest_path_graph.h"
 
 #include <algorithm>
+
+void shortest_path_grapht::get_path_lengths_in_function()
+{
+  bool found_property = false;
+  bool found_end = false;
+  node_indext end_index;
+  node_indext property_index;
+  node_indext index = 0;
+  for(auto &n : nodes)
+  {
+    if(n.PC->is_assert())
+    {
+      if(found_property == false)
+      {
+        n.is_property = true;
+        n.shortest_path_to_property = 0;
+        found_property = true;
+        property_index = index;
+      }
+      else
+        throw "shortest path search cannot be used with multiple properties";
+    }
+    if(n.PC->is_end_function())
+    {
+      end_index = index;
+      found_end = true;
+    }
+    index++;
+  }
+
+  if(!found_property)
+  {
+    nodes[end_index].shortest_path_to_property = 0;
+    bfs(end_index);
+  }
+  else
+    bfs(property_index);
+
+  write_lengths_to_locs();
+}
+
+void per_function_shortest_patht::build(const goto_functionst &goto_functions)
+{
+  forall_goto_functions(it, goto_functions)
+    if(it->second.body_available())
+    {
+      shortest_path_grapht path_graph(it->second.body, locs);
+    }
+}
+
 void shortest_path_grapht::bfs(node_indext property_index)
 {
   // does BFS, not Dijkstra
diff --git a/src/symex/shortest_path_graph.h b/src/symex/shortest_path_graph.h
index 813540b..9d1547e 100644
--- a/src/symex/shortest_path_graph.h
+++ b/src/symex/shortest_path_graph.h
@@ -49,6 +49,15 @@ class shortest_path_grapht: public cfg_baset<shortest_path_nodet>
     get_path_lengths_to_property();
     }
 
+  explicit shortest_path_grapht(
+      const goto_programt &_goto_program, locst &_locs):
+    locs(_locs),
+    target_to_loc_map(_locs)
+    {
+    cfg_baset<shortest_path_nodet>::operator()(_goto_program);
+    get_path_lengths_in_function();
+    }
+
 protected:
   /// \brief writes the computed shortest path for every node
   /// in the graph to the corresponding location in locst.
@@ -60,6 +69,11 @@ class shortest_path_grapht: public cfg_baset<shortest_path_nodet>
   /// is present, we use the first one discovered.
   /// Calls bfs() to do this.
   void get_path_lengths_to_property();
+  /// \brief computes the shortest path from every node in a
+  /// graph to the property, or the end of the funciton if
+  /// there is no property.
+  /// we assume the graph is a graph of a single function.
+  void get_path_lengths_in_function();
   /// \brief implements backwards BFS to compute distance from every node in
   /// the graph to the node index given as parameter
   /// \param destination node index
@@ -69,4 +83,27 @@ class shortest_path_grapht: public cfg_baset<shortest_path_nodet>
   target_to_loc_mapt target_to_loc_map;
 };
 
+/// \brief class contains CFG of program locations
+/// for every function with the shortest distance to a
+/// property, or the end of a function, calculated for each location
+/// The distances computed for each node are written to the corresponding
+/// loct in the locst passed as param to the constructor. This allows us
+/// to use these numbers to guide a symex search
+/// \param goto functions to create the CFGs from, locs struct made from the
+/// same goto_functions
+class per_function_shortest_patht
+{
+public:
+  explicit per_function_shortest_patht(
+      const goto_functionst &_goto_functions, locst &_locs):
+  locs(_locs)
+  {
+    build(_goto_functions);
+  }
+
+protected:
+  locst &locs;
+  void build(const goto_functionst & goto_functions);
+};
+
 #endif /* CPROVER_SYMEX_SHORTEST_PATH_GRAPH_H */

From 30961902f194fabb9024e37fcfee2b0e4558f840 Mon Sep 17 00:00:00 2001
From: polgreen <polgreen@amazon.com>
Date: Thu, 19 Oct 2017 14:51:48 +0200
Subject: [PATCH 06/12] Output distances to property from every reachable
 program location

---
 src/path-symex/locs.cpp           | 33 +++++++++++++++++++++++++++++++
 src/path-symex/locs.h             |  1 +
 src/symex/symex_parse_options.cpp | 15 ++++++++++++++
 src/symex/symex_parse_options.h   |  1 +
 4 files changed, 50 insertions(+)

diff --git a/src/path-symex/locs.cpp b/src/path-symex/locs.cpp
index ef1026f..bcd4eaf 100644
--- a/src/path-symex/locs.cpp
+++ b/src/path-symex/locs.cpp
@@ -82,6 +82,39 @@ void locst::build(const goto_functionst &goto_functions)
   }
 }
 
+void locst::output_reachable(std::ostream &out) const
+{
+  irep_idt function;
+  int reachable_count = 0;
+  int unreachable_count = 0;
+
+  for(unsigned l = 0; l < loc_vector.size(); l++)
+  {
+    const loct &loc = loc_vector[l];
+    if(loc.distance_to_property != -1)
+    {
+      reachable_count++;
+      if(function != loc.function)
+      {
+        function = loc.function;
+        out << "*** " << function << "\n";
+      }
+
+      out << "  L" << l << ": " << " " << as_string(ns, *loc.target)
+          << " path length: " << loc_vector[l].distance_to_property << "\n";
+
+      if(!loc.branch_target.is_nil())
+        out << "    T: " << loc.branch_target << "\n";
+    }
+    else
+      unreachable_count++;
+  }
+  out << "\n";
+  out << "The entry location is L" << entry_loc << ".\n";
+  out << "Number of reachable locs " << reachable_count << "\n";
+  out << "Number of unreachable locs " << unreachable_count << "\n";
+}
+
 void locst::output(std::ostream &out) const
 {
   irep_idt function;
diff --git a/src/path-symex/locs.h b/src/path-symex/locs.h
index c3578c2..1ec7c97 100644
--- a/src/path-symex/locs.h
+++ b/src/path-symex/locs.h
@@ -59,6 +59,7 @@ class locst
   explicit locst(const namespacet &_ns);
   void build(const goto_functionst &goto_functions);
   void output(std::ostream &out) const;
+  void output_reachable(std::ostream &out) const;
 
   loct &operator[] (loc_reft l)
   {
diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index b2a7243..f4dbd7c 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -58,6 +58,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <path-symex/locs.h>
 
 #include "path_search.h"
+#include "shortest_path_graph.h"
 
 symex_parse_optionst::symex_parse_optionst(int argc, const char **argv):
   parse_options_baset(SYMEX_OPTIONS, argc, argv),
@@ -202,6 +203,18 @@ int symex_parse_optionst::doit()
     return 0;
   }
 
+  if(cmdline.isset("show-distances-to-property"))
+  {
+    const namespacet ns(goto_model.symbol_table);
+    locst locs(ns);
+    locs.build(goto_model.goto_functions);
+
+    shortest_path_grapht path_search_graph(goto_model.goto_functions, locs);
+
+    locs.output_reachable(std::cout);
+    return 0;
+  }
+
   // do actual Symex
 
   try
@@ -647,6 +660,8 @@ void symex_parse_optionst::help()
     " --eager-infeasibility        query solver early to determine whether a path is infeasible before searching it\n" // NOLINT(*)
     "\n"
     "Other options:\n"
+    " --show-distances-to-property\n"
+    "                              shows the (context free) shortest path from every reachable program location to a single property" // NOLINT(*)
     " --version                    show version and exit\n"
     " --xml-ui                     use XML-formatted output\n"
     " --verbosity #                verbosity level\n"
diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h
index 066b83e..b5bf54f 100644
--- a/src/symex/symex_parse_options.h
+++ b/src/symex/symex_parse_options.h
@@ -51,6 +51,7 @@ class optionst;
   "(show-locs)(show-vcc)(show-properties)(show-symbol-table)" \
   "(drop-unused-functions)" \
   "(object-bits):" \
+  "(show-distances-to-property)" \
   OPT_SHOW_GOTO_FUNCTIONS \
   "(property):(trace)(show-trace)(stop-on-fail)(eager-infeasibility)" \
   "(no-simplify)(no-unwinding-assertions)(no-propagation)" \

From 5ad8ef3b699ebda39af8d01a0470a4786bef4f65 Mon Sep 17 00:00:00 2001
From: polgreen <polgreen@amazon.com>
Date: Thu, 19 Oct 2017 15:57:58 +0200
Subject: [PATCH 07/12] access shortest path locst variable from
 path_symex_statet

---
 src/path-symex/path_symex_state.h | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/path-symex/path_symex_state.h b/src/path-symex/path_symex_state.h
index fc3597d..3b042ff 100644
--- a/src/path-symex/path_symex_state.h
+++ b/src/path-symex/path_symex_state.h
@@ -208,6 +208,11 @@ struct path_symex_statet
     return depth;
   }
 
+  unsigned get_shortest_path() const
+  {
+    return locs.loc_vector[pc().loc_number].distance_to_property;
+  }
+
   void increase_depth()
   {
     depth++;

From 68edca7754a5fc2cc6568594c55dc523a5137305 Mon Sep 17 00:00:00 2001
From: polgreen <polgreen@amazon.com>
Date: Thu, 19 Oct 2017 15:57:34 +0200
Subject: [PATCH 08/12] Shortest path search heuristic

Shortest path search heuristic computes the shortest path from all program locations to a single property. This metric is used to guide the symex search.

We also introduce randomized shortest path based search, which makes a random choice when picking the next state every 1000 choices in order to avoid local minima
---
 src/symex/path_search.cpp         | 73 +++++++++++++++++++++++++++++--
 src/symex/path_search.h           | 11 ++++-
 src/symex/symex_parse_options.cpp | 11 ++++-
 src/symex/symex_parse_options.h   |  2 +-
 4 files changed, 90 insertions(+), 7 deletions(-)

diff --git a/src/symex/path_search.cpp b/src/symex/path_search.cpp
index 9ca139b..b129c14 100644
--- a/src/symex/path_search.cpp
+++ b/src/symex/path_search.cpp
@@ -20,8 +20,51 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <path-symex/path_symex.h>
 #include <path-symex/build_goto_trace.h>
 
+#include "shortest_path_graph.h"
+
 #include <random>
 
+
+void path_searcht::sort_queue()
+{
+  debug()<< " get shortest path, queue.size = " <<queue.size() <<eom;
+  if(queue.size()==1)
+  {
+    current_distance = queue.front().get_shortest_path();
+    return;
+  }
+
+  unsigned shortest_path = std::numeric_limits<unsigned>::max();
+
+  std::list<statet>::iterator it;
+  std::list<statet>::iterator closest_state;
+
+  for(it=queue.begin(); it!=queue.end(); ++it)
+  {
+    if(it->get_shortest_path() < shortest_path)
+    {
+      shortest_path = it->get_shortest_path();
+      closest_state = it;
+    }
+  }
+
+  if(shortest_path != std::numeric_limits<unsigned>::max())
+  {
+    current_distance = shortest_path;
+    statet tmp = *closest_state;
+    queue.erase(closest_state);
+    queue.push_front(tmp);
+  }
+  else
+  {
+    error() << "all states have shortest path length = MAX_UNSIGNED_INT, "
+             << "try removing function pointers with goto-instrument next time."
+             << "randomly picking state instead"
+             << eom;
+    shuffle_queue(queue);
+  }
+}
+
 void path_searcht::shuffle_queue(queuet &queue)
 {
   if(queue.size()<=1)
@@ -54,9 +97,8 @@ path_searcht::resultt path_searcht::operator()(
   // this is the container for the history-forest
   path_symex_historyt history;
 
-  queue.push_back(initial_state(var_map, locs, history));
-
   // set up the statistics
+  current_distance = std::numeric_limits<unsigned>::max();
   number_of_dropped_states=0;
   number_of_paths=0;
   number_of_VCCs=0;
@@ -72,6 +114,15 @@ path_searcht::resultt path_searcht::operator()(
   absolute_timet last_reported_time=start_time;
 
   initialize_property_map(goto_functions);
+  if(search_heuristic == search_heuristict::SHORTEST_PATH ||
+      search_heuristic == search_heuristict::RAN_SHORTEST_PATH )
+  {
+    status()<<"Building shortest path graph" << eom;
+    shortest_path_grapht shortest_path_graph(goto_functions, locs);
+  }
+  statet init_state = initial_state(var_map, locs, history);
+  queue.push_back(init_state);
+  initial_distance_to_property=init_state.get_shortest_path();
 
   while(!queue.empty())
   {
@@ -135,8 +186,13 @@ path_searcht::resultt path_searcht::operator()(
                    << " thread " << state.get_current_thread()+1
                    << '/' << state.threads.size()
                    << " PC " << state.pc()
-                   << " depth " << state.get_depth()
-                   << " [" << number_of_steps << " steps, "
+                   << " depth " << state.get_depth();
+
+          if(search_heuristic == search_heuristict::SHORTEST_PATH
+              || search_heuristic == search_heuristict::RAN_SHORTEST_PATH)
+            status() << " distance to property " << state.get_shortest_path();
+
+          status() << " [" << number_of_steps << " steps, "
                    << running_time << "s]" << messaget::eom;
         }
       }
@@ -243,6 +299,15 @@ void path_searcht::pick_state()
       queue.splice(queue.begin(), queue, --queue.end(), queue.end());
     return;
 
+  case search_heuristict::RAN_SHORTEST_PATH:
+    if(number_of_steps%1000==0)
+      shuffle_queue(queue);
+    else
+      sort_queue();
+    return;
+  case search_heuristict::SHORTEST_PATH:
+    sort_queue();
+    return;
   case search_heuristict::LOCS:
     return;
   }
diff --git a/src/symex/path_search.h b/src/symex/path_search.h
index aa3a39d..3df961d 100644
--- a/src/symex/path_search.h
+++ b/src/symex/path_search.h
@@ -80,6 +80,8 @@ class path_searcht:public safety_checkert
   bool stop_on_fail;
 
   // statistics
+  unsigned current_distance;
+  unsigned initial_distance_to_property;
   std::size_t number_of_dropped_states;
   std::size_t number_of_paths;
   std::size_t number_of_steps;
@@ -110,6 +112,10 @@ class path_searcht:public safety_checkert
   void set_randomized_dfs() { search_heuristic=search_heuristict::RAN_DFS; }
   void set_bfs() { search_heuristic=search_heuristict::BFS; }
   void set_locs() { search_heuristic=search_heuristict::LOCS; }
+  void set_shortest_path()
+    { search_heuristic=search_heuristict::SHORTEST_PATH; }
+  void set_ran_shortest_path()
+    { search_heuristic=search_heuristict::RAN_SHORTEST_PATH; }
 
   typedef std::map<irep_idt, property_entryt> property_mapt;
   property_mapt property_map;
@@ -124,6 +130,9 @@ class path_searcht:public safety_checkert
   /// Pick random element of queue and move to front
   /// \param queue  queue to be shuffled
   void shuffle_queue(queuet &queue);
+  /// Move element with shortest distance to property
+  /// to the front of the queue
+  void sort_queue();
   // search heuristic
   void pick_state();
 
@@ -155,7 +164,7 @@ class path_searcht:public safety_checkert
   unsigned time_limit;
 
   enum class search_heuristict
-  { DFS, RAN_DFS, BFS, LOCS } search_heuristic;
+  { DFS, RAN_DFS, BFS, LOCS, SHORTEST_PATH, RAN_SHORTEST_PATH } search_heuristic;
 
   source_locationt last_source_location;
 };
diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index f4dbd7c..8ae67ba 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -258,6 +258,13 @@ int symex_parse_optionst::doit()
     if(cmdline.isset("locs"))
       path_search.set_locs();
 
+    if(cmdline.isset("shortest-path"))
+    {
+      if(cmdline.isset("randomize"))
+        path_search.set_ran_shortest_path();
+      else
+        path_search.set_shortest_path();
+    }
     if(cmdline.isset("show-vcc"))
     {
       path_search.show_vcc=true;
@@ -656,7 +663,9 @@ void symex_parse_optionst::help()
     " --max-search-time s          limit search to approximately s seconds\n"
     " --dfs                        use depth first search\n"
     " --bfs                        use breadth first search\n"
-    " --randomize                  used in conjunction with dfs, to search by randomized dfs\n" // NOLINT(*)
+    "--shortest-path               use shortest path guided search\n"
+    " --randomize                  in conjunction with dfs to use randomized dfs\n" // NOLINT(*)
+	  "                              in conjunction with shortest path to use randomized shortest path guided search\n" // NOLINT(*)
     " --eager-infeasibility        query solver early to determine whether a path is infeasible before searching it\n" // NOLINT(*)
     "\n"
     "Other options:\n"
diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h
index b5bf54f..05deb6b 100644
--- a/src/symex/symex_parse_options.h
+++ b/src/symex/symex_parse_options.h
@@ -40,7 +40,7 @@ class optionst;
   "(little-endian)(big-endian)" \
   "(error-label):(verbosity):(no-library)" \
   "(version)" \
-  "(bfs)(dfs)(locs)" \
+  "(bfs)(dfs)(locs)(shortest-path)" \
   "(randomize)" \
   "(cover):" \
   "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \

From 115037d35da51fb9fe5df513ff3de09303cb465f Mon Sep 17 00:00:00 2001
From: polgreen <polgreen@amazon.com>
Date: Thu, 19 Oct 2017 16:19:07 +0200
Subject: [PATCH 09/12] Shortest path per function search heuristic

Computes the shortest path per function on the shortest path graph and uses this heuristic to guide the symex search
---
 src/symex/path_search.cpp         | 45 +++++++++++++++++++++++++++++++
 src/symex/path_search.h           |  6 ++++-
 src/symex/symex_parse_options.cpp |  5 ++++
 src/symex/symex_parse_options.h   |  1 +
 4 files changed, 56 insertions(+), 1 deletion(-)

diff --git a/src/symex/path_search.cpp b/src/symex/path_search.cpp
index b129c14..188cc9e 100644
--- a/src/symex/path_search.cpp
+++ b/src/symex/path_search.cpp
@@ -65,6 +65,42 @@ void path_searcht::sort_queue()
   }
 }
 
+// We prioritise remaining in the same function, but if there is no choice
+// we take the next state with the shortest path
+void path_searcht::sort_queue_per_function()
+{
+  debug()<< " get shortest path, queue.size = " <<queue.size() <<eom;
+  if(queue.size()==1)
+  {
+    current_distance = queue.front().get_shortest_path();
+    return;
+  }
+
+  unsigned shortest_path = std::numeric_limits<unsigned>::max();
+
+  std::list<statet>::iterator it;
+  std::list<statet>::iterator closest_state;
+
+  // pick the first state in the queue that is a direct successor, i.e.,
+  // has a path length 1 less than the current path length
+  for(it=queue.begin(); it!=queue.end(); ++it)
+  {
+    if(it->get_shortest_path()+1 == current_distance)
+    {
+      shortest_path = it->get_shortest_path();
+      current_distance = shortest_path;
+      statet tmp = *it;
+      queue.erase(it);
+      queue.push_front(tmp);
+      return;
+    }
+  }
+
+  // if we get here there was no direct successor, we revert to
+  // picking the shortest path
+  sort_queue();
+}
+
 void path_searcht::shuffle_queue(queuet &queue)
 {
   if(queue.size()<=1)
@@ -120,6 +156,12 @@ path_searcht::resultt path_searcht::operator()(
     status()<<"Building shortest path graph" << eom;
     shortest_path_grapht shortest_path_graph(goto_functions, locs);
   }
+  else if(search_heuristic == search_heuristict::SHORTEST_PATH_PER_FUNC)
+  {
+    status()<<"Building shortest path graph per function" << eom;
+    per_function_shortest_patht shortest_path_graph(goto_functions, locs);
+  }
+
   statet init_state = initial_state(var_map, locs, history);
   queue.push_back(init_state);
   initial_distance_to_property=init_state.get_shortest_path();
@@ -308,6 +350,9 @@ void path_searcht::pick_state()
   case search_heuristict::SHORTEST_PATH:
     sort_queue();
     return;
+  case search_heuristict::SHORTEST_PATH_PER_FUNC:
+    sort_queue_per_function();
+    return;
   case search_heuristict::LOCS:
     return;
   }
diff --git a/src/symex/path_search.h b/src/symex/path_search.h
index 3df961d..4a112a8 100644
--- a/src/symex/path_search.h
+++ b/src/symex/path_search.h
@@ -116,6 +116,8 @@ class path_searcht:public safety_checkert
     { search_heuristic=search_heuristict::SHORTEST_PATH; }
   void set_ran_shortest_path()
     { search_heuristic=search_heuristict::RAN_SHORTEST_PATH; }
+  void set_shortest_path_per_function()
+    { search_heuristic=search_heuristict::SHORTEST_PATH_PER_FUNC; }
 
   typedef std::map<irep_idt, property_entryt> property_mapt;
   property_mapt property_map;
@@ -133,6 +135,7 @@ class path_searcht:public safety_checkert
   /// Move element with shortest distance to property
   /// to the front of the queue
   void sort_queue();
+  void sort_queue_per_function();
   // search heuristic
   void pick_state();
 
@@ -164,7 +167,8 @@ class path_searcht:public safety_checkert
   unsigned time_limit;
 
   enum class search_heuristict
-  { DFS, RAN_DFS, BFS, LOCS, SHORTEST_PATH, RAN_SHORTEST_PATH } search_heuristic;
+  { DFS, RAN_DFS, BFS, LOCS, SHORTEST_PATH,
+    RAN_SHORTEST_PATH , SHORTEST_PATH_PER_FUNC } search_heuristic;
 
   source_locationt last_source_location;
 };
diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index 8ae67ba..8542cb5 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -265,6 +265,10 @@ int symex_parse_optionst::doit()
       else
         path_search.set_shortest_path();
     }
+
+    if(cmdline.isset("shortest-path-per-function"))
+      path_search.set_shortest_path_per_function();
+
     if(cmdline.isset("show-vcc"))
     {
       path_search.show_vcc=true;
@@ -664,6 +668,7 @@ void symex_parse_optionst::help()
     " --dfs                        use depth first search\n"
     " --bfs                        use breadth first search\n"
     "--shortest-path               use shortest path guided search\n"
+    "--shortest-path-per-function  computes shortest path locally and uses to guide symex search\n" // NOLINT(*)
     " --randomize                  in conjunction with dfs to use randomized dfs\n" // NOLINT(*)
 	  "                              in conjunction with shortest path to use randomized shortest path guided search\n" // NOLINT(*)
     " --eager-infeasibility        query solver early to determine whether a path is infeasible before searching it\n" // NOLINT(*)
diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h
index 05deb6b..e55d6ee 100644
--- a/src/symex/symex_parse_options.h
+++ b/src/symex/symex_parse_options.h
@@ -41,6 +41,7 @@ class optionst;
   "(error-label):(verbosity):(no-library)" \
   "(version)" \
   "(bfs)(dfs)(locs)(shortest-path)" \
+  "(shortest-path-per-function)" \
   "(randomize)" \
   "(cover):" \
   "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \

From e336d70a315b958d1e0c048a41e25208b0fef469 Mon Sep 17 00:00:00 2001
From: polgreen <polgreen@amazon.com>
Date: Thu, 19 Oct 2017 18:39:24 +0200
Subject: [PATCH 10/12] Output search heuristic and initialisation time

---
 src/symex/path_search.cpp | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/src/symex/path_search.cpp b/src/symex/path_search.cpp
index 188cc9e..ca3a6a3 100644
--- a/src/symex/path_search.cpp
+++ b/src/symex/path_search.cpp
@@ -130,6 +130,31 @@ path_searcht::resultt path_searcht::operator()(
 
   status() << "Starting symbolic simulation" << eom;
 
+  switch(search_heuristic)
+  {
+  case search_heuristict::DFS:
+    status() << "Search heuristic: DFS" << eom;
+    break;
+  case search_heuristict::RAN_DFS:
+    status() << "Search heuristic: randomized DFS" << eom;
+    break;
+  case search_heuristict::BFS:
+    status() << "Search heuristic: BFS" << eom;
+    break;
+  case search_heuristict::SHORTEST_PATH:
+    status() << "Search heuristic: shortest path" << eom;
+    break;
+  case search_heuristict::SHORTEST_PATH_PER_FUNC:
+    status() << "Search heuristic: shortest path per function" << eom;
+    break;
+  case search_heuristict::RAN_SHORTEST_PATH:
+    status() << "Search heuristic: randomized shortest path" << eom;
+    break;
+  case search_heuristict::LOCS:
+    status() << "Search heuristic: LOCS" << eom;
+    break;
+  }
+
   // this is the container for the history-forest
   path_symex_historyt history;
 
@@ -166,6 +191,11 @@ path_searcht::resultt path_searcht::operator()(
   queue.push_back(init_state);
   initial_distance_to_property=init_state.get_shortest_path();
 
+  time_periodt initialisation_time=current_time()-start_time;
+  status() << "Initialisation took "<< initialisation_time << "s" << eom;
+  start_time=current_time();
+  last_reported_time=start_time;
+
   while(!queue.empty())
   {
     number_of_steps++;

From cd4a73a3603c1c2b67c7d154eb83c0ac9bdf2ecd Mon Sep 17 00:00:00 2001
From: polgreen <polgreen@amazon.com>
Date: Sat, 21 Oct 2017 12:46:24 +0200
Subject: [PATCH 11/12] Regression tests for symex shortest path search
 heuristics

This is all the regression tests from regression/symex that only have one property, and all the regression tests from regression/symex-infeasibility that the default symex search heuristic (dfs) can complete in a reasonable amount of time.
---
 regression/symex-shortest-path/Makefile       |  22 +++
 .../symex-shortest-path/bst-safe/main.c       | 101 ++++++++++++++
 .../symex-shortest-path/bst-safe/test.desc    |   8 ++
 .../concrete-sum-unsafe/main.c                |  18 +++
 .../concrete-sum-unsafe/test.desc             |   6 +
 .../concrete-sum/concrete-sum-unsafe.c        |  16 +++
 .../symex-shortest-path/concrete-sum/main.c   |  21 +++
 .../concrete-sum/test.desc                    |   8 ++
 .../symex-shortest-path/counter-unsafe/main.c |  39 ++++++
 .../counter-unsafe/test.desc                  |   6 +
 .../symex-shortest-path/for-loop/main.c       |  13 ++
 .../symex-shortest-path/for-loop/test.desc    |   8 ++
 .../function_pointer1/main.c                  |  32 +++++
 .../function_pointer1/test.desc               |   8 ++
 .../insertion-sort-unsafe/main.c              |  47 +++++++
 .../insertion-sort-unsafe/test.desc           |   6 +
 .../symex-shortest-path/modulus-safe/main.c   |  38 ++++++
 .../modulus-safe/test.desc                    |   8 ++
 .../symex-shortest-path/modulus-unsafe/main.c |  31 +++++
 .../modulus-unsafe/test.desc                  |   6 +
 .../symex-shortest-path/pointer2/main.c       |  31 +++++
 .../symex-shortest-path/pointer2/test.desc    |   8 ++
 .../symex-shortest-path/pointer3/main.c       |  14 ++
 .../symex-shortest-path/pointer3/test.desc    |   8 ++
 .../symex-shortest-path/show-trace1/main.c    |  15 ++
 .../symex-shortest-path/show-trace1/test.desc |  11 ++
 .../symex-shortest-path/stop-on-fail1/main.c  |  12 ++
 .../stop-on-fail1/test.desc                   |   9 ++
 regression/symex-shortest-path/struct1/main.c |  25 ++++
 .../symex-shortest-path/struct1/test.desc     |   8 ++
 regression/symex-shortest-path/struct2/main.c |  18 +++
 .../symex-shortest-path/struct2/test.desc     |   8 ++
 regression/symex-shortest-path/struct3/main.c |  37 +++++
 .../symex-shortest-path/struct3/test.desc     |   8 ++
 regression/symex-shortest-path/tp1/main.c     | 127 +++++++++++++++++
 regression/symex-shortest-path/tp1/test.desc  |   8 ++
 regression/symex-shortest-path/tp2/main.c     |  57 ++++++++
 regression/symex-shortest-path/tp2/test.desc  |   8 ++
 regression/symex-shortest-path/tp3/main.c     | 129 ++++++++++++++++++
 regression/symex-shortest-path/tp3/test.desc  |   8 ++
 regression/symex-shortest-path/tp4/main.c     |  60 ++++++++
 regression/symex-shortest-path/tp4/test.desc  |   8 ++
 .../symex-shortest-path/va_args_1/main.c      |  37 +++++
 .../symex-shortest-path/va_args_1/test.desc   |   8 ++
 .../symex-shortest-path/va_args_10/main.c     |  41 ++++++
 .../symex-shortest-path/va_args_10/test.desc  |   8 ++
 .../symex-shortest-path/va_args_11/main.c     |  29 ++++
 .../symex-shortest-path/va_args_11/test.desc  |   8 ++
 .../symex-shortest-path/va_args_2/main.c      |  35 +++++
 .../symex-shortest-path/va_args_2/test.desc   |   8 ++
 .../symex-shortest-path/va_args_3/main.c      |  34 +++++
 .../symex-shortest-path/va_args_3/test.desc   |   8 ++
 .../symex-shortest-path/va_args_4/main.c      |  38 ++++++
 .../symex-shortest-path/va_args_4/test.desc   |   8 ++
 .../symex-shortest-path/va_args_5/main.c      |  35 +++++
 .../symex-shortest-path/va_args_5/test.desc   |   6 +
 .../symex-shortest-path/va_args_6/main.c      |  34 +++++
 .../symex-shortest-path/va_args_6/test.desc   |   6 +
 .../symex-shortest-path/va_args_7/main.c      |  23 ++++
 .../symex-shortest-path/va_args_7/test.desc   |   6 +
 .../symex-shortest-path/va_args_8/main.c      |  37 +++++
 .../symex-shortest-path/va_args_8/test.desc   |   8 ++
 .../symex-shortest-path/va_args_9/main.c      |  41 ++++++
 .../symex-shortest-path/va_args_9/test.desc   |   8 ++
 64 files changed, 1525 insertions(+)
 create mode 100644 regression/symex-shortest-path/Makefile
 create mode 100644 regression/symex-shortest-path/bst-safe/main.c
 create mode 100644 regression/symex-shortest-path/bst-safe/test.desc
 create mode 100644 regression/symex-shortest-path/concrete-sum-unsafe/main.c
 create mode 100644 regression/symex-shortest-path/concrete-sum-unsafe/test.desc
 create mode 100644 regression/symex-shortest-path/concrete-sum/concrete-sum-unsafe.c
 create mode 100644 regression/symex-shortest-path/concrete-sum/main.c
 create mode 100644 regression/symex-shortest-path/concrete-sum/test.desc
 create mode 100644 regression/symex-shortest-path/counter-unsafe/main.c
 create mode 100644 regression/symex-shortest-path/counter-unsafe/test.desc
 create mode 100644 regression/symex-shortest-path/for-loop/main.c
 create mode 100644 regression/symex-shortest-path/for-loop/test.desc
 create mode 100644 regression/symex-shortest-path/function_pointer1/main.c
 create mode 100644 regression/symex-shortest-path/function_pointer1/test.desc
 create mode 100644 regression/symex-shortest-path/insertion-sort-unsafe/main.c
 create mode 100644 regression/symex-shortest-path/insertion-sort-unsafe/test.desc
 create mode 100644 regression/symex-shortest-path/modulus-safe/main.c
 create mode 100644 regression/symex-shortest-path/modulus-safe/test.desc
 create mode 100644 regression/symex-shortest-path/modulus-unsafe/main.c
 create mode 100644 regression/symex-shortest-path/modulus-unsafe/test.desc
 create mode 100644 regression/symex-shortest-path/pointer2/main.c
 create mode 100644 regression/symex-shortest-path/pointer2/test.desc
 create mode 100644 regression/symex-shortest-path/pointer3/main.c
 create mode 100644 regression/symex-shortest-path/pointer3/test.desc
 create mode 100644 regression/symex-shortest-path/show-trace1/main.c
 create mode 100644 regression/symex-shortest-path/show-trace1/test.desc
 create mode 100644 regression/symex-shortest-path/stop-on-fail1/main.c
 create mode 100644 regression/symex-shortest-path/stop-on-fail1/test.desc
 create mode 100644 regression/symex-shortest-path/struct1/main.c
 create mode 100644 regression/symex-shortest-path/struct1/test.desc
 create mode 100644 regression/symex-shortest-path/struct2/main.c
 create mode 100644 regression/symex-shortest-path/struct2/test.desc
 create mode 100644 regression/symex-shortest-path/struct3/main.c
 create mode 100644 regression/symex-shortest-path/struct3/test.desc
 create mode 100644 regression/symex-shortest-path/tp1/main.c
 create mode 100644 regression/symex-shortest-path/tp1/test.desc
 create mode 100644 regression/symex-shortest-path/tp2/main.c
 create mode 100644 regression/symex-shortest-path/tp2/test.desc
 create mode 100644 regression/symex-shortest-path/tp3/main.c
 create mode 100644 regression/symex-shortest-path/tp3/test.desc
 create mode 100644 regression/symex-shortest-path/tp4/main.c
 create mode 100644 regression/symex-shortest-path/tp4/test.desc
 create mode 100644 regression/symex-shortest-path/va_args_1/main.c
 create mode 100644 regression/symex-shortest-path/va_args_1/test.desc
 create mode 100644 regression/symex-shortest-path/va_args_10/main.c
 create mode 100644 regression/symex-shortest-path/va_args_10/test.desc
 create mode 100644 regression/symex-shortest-path/va_args_11/main.c
 create mode 100644 regression/symex-shortest-path/va_args_11/test.desc
 create mode 100644 regression/symex-shortest-path/va_args_2/main.c
 create mode 100644 regression/symex-shortest-path/va_args_2/test.desc
 create mode 100644 regression/symex-shortest-path/va_args_3/main.c
 create mode 100644 regression/symex-shortest-path/va_args_3/test.desc
 create mode 100644 regression/symex-shortest-path/va_args_4/main.c
 create mode 100644 regression/symex-shortest-path/va_args_4/test.desc
 create mode 100644 regression/symex-shortest-path/va_args_5/main.c
 create mode 100644 regression/symex-shortest-path/va_args_5/test.desc
 create mode 100644 regression/symex-shortest-path/va_args_6/main.c
 create mode 100644 regression/symex-shortest-path/va_args_6/test.desc
 create mode 100644 regression/symex-shortest-path/va_args_7/main.c
 create mode 100644 regression/symex-shortest-path/va_args_7/test.desc
 create mode 100644 regression/symex-shortest-path/va_args_8/main.c
 create mode 100644 regression/symex-shortest-path/va_args_8/test.desc
 create mode 100644 regression/symex-shortest-path/va_args_9/main.c
 create mode 100644 regression/symex-shortest-path/va_args_9/test.desc

diff --git a/regression/symex-shortest-path/Makefile b/regression/symex-shortest-path/Makefile
new file mode 100644
index 0000000..c21125c
--- /dev/null
+++ b/regression/symex-shortest-path/Makefile
@@ -0,0 +1,22 @@
+default: tests.log
+
+test:
+	@../test.pl -c "../../../src/symex/symex --shortest-path"
+	@../test.pl -c "../../../src/symex/symex --shortest-path --randomize"
+
+tests.log: ../test.pl
+	@../test.pl -c "../../../src/symex/symex --shortest-path"
+	@../test.pl -c "../../../src/symex/symex --shortest-path --randomize"
+
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) '{}' \;
+	$(RM) tests.log
diff --git a/regression/symex-shortest-path/bst-safe/main.c b/regression/symex-shortest-path/bst-safe/main.c
new file mode 100644
index 0000000..868a204
--- /dev/null
+++ b/regression/symex-shortest-path/bst-safe/main.c
@@ -0,0 +1,101 @@
+// This file contains code snippets from "Algorithms in C, Third Edition,
+// Parts 1-4," by Robert Sedgewick.
+//
+// See https://www.cs.princeton.edu/~rs/Algs3.c1-4/code.txt
+
+#include <stdlib.h>
+#include <assert.h>
+
+#define N 1000
+
+
+#ifdef ENABLE_KLEE
+#include <klee/klee.h>
+#endif
+
+typedef int Key;
+typedef int Item;
+
+#define eq(A, B) (!less(A, B) && !less(B, A))
+#define key(A) (A)
+#define less(A, B) (key(A) < key(B))
+#define NULLitem 0
+
+struct STnode;
+typedef struct STnode* link;
+
+struct STnode { Item item; link l, r; int n; };
+static link head, z;
+
+static link NEW(Item item, link l, link r, int n) {
+  link x = malloc(sizeof *x);
+  x->item = item; x->l = l; x->r = r; x->n = n;
+  return x;
+}
+
+void STinit() {
+  head = (z = NEW(NULLitem, 0, 0, 0));
+}
+
+int STcount() { return head->n; }
+
+static link insertR(link h, Item item) {
+  Key v = key(item), t = key(h->item);
+  if (h == z) return NEW(item, z, z, 1);
+
+  if (less(v, t))
+    h->l = insertR(h->l, item);
+  else
+    h->r = insertR(h->r, item);
+
+  (h->n)++; return h;
+}
+
+void STinsert(Item item) { head = insertR(head, item); }
+
+static void sortR(link h, void (*visit)(Item)) {
+  if (h == z) return;
+  sortR(h->l, visit);
+  visit(h->item);
+  sortR(h->r, visit);
+}
+
+void STsort(void (*visit)(Item)) { sortR(head, visit); }
+
+
+static Item a[N];
+static unsigned k = 0;
+void sorter(Item item) {
+  a[k++] = item;
+}
+
+#ifdef ENABLE_CPROVER
+int nondet_int();
+#endif
+
+// Unwind N+1 times
+int main() {
+#ifdef ENABLE_KLEE
+  klee_make_symbolic(a, sizeof(a), "a");
+#endif
+
+  STinit();
+
+  for (unsigned i = 0; i < N; i++) {
+#ifdef ENABLE_CPROVER
+    STinsert(nondet_int());
+#elif ENABLE_KLEE
+    STinsert(a[i]);
+    a[i] = NULLitem;
+#endif
+  }
+
+  STsort(sorter);
+
+#ifndef FORCE_BRANCH
+  for (unsigned i = 0; i < N - 1; i++)
+    assert(a[i] <= a[i+1]);
+#endif
+
+  return 0;
+}
diff --git a/regression/symex-shortest-path/bst-safe/test.desc b/regression/symex-shortest-path/bst-safe/test.desc
new file mode 100644
index 0000000..9efefbc
--- /dev/null
+++ b/regression/symex-shortest-path/bst-safe/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/concrete-sum-unsafe/main.c b/regression/symex-shortest-path/concrete-sum-unsafe/main.c
new file mode 100644
index 0000000..42feb3f
--- /dev/null
+++ b/regression/symex-shortest-path/concrete-sum-unsafe/main.c
@@ -0,0 +1,18 @@
+#include <assert.h>
+
+#define N 40000
+
+int main(void) {
+  unsigned n = 1;
+  unsigned sum = 0;
+
+  while (n <= N)
+  {
+    sum = sum + n;
+    n = n + 1;
+  }
+
+  assert(sum != ((N * (N + 1)) / 2));
+
+  return 0;
+}
diff --git a/regression/symex-shortest-path/concrete-sum-unsafe/test.desc b/regression/symex-shortest-path/concrete-sum-unsafe/test.desc
new file mode 100644
index 0000000..510460c
--- /dev/null
+++ b/regression/symex-shortest-path/concrete-sum-unsafe/test.desc
@@ -0,0 +1,6 @@
+CORE
+main.c
+
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/concrete-sum/concrete-sum-unsafe.c b/regression/symex-shortest-path/concrete-sum/concrete-sum-unsafe.c
new file mode 100644
index 0000000..584f997
--- /dev/null
+++ b/regression/symex-shortest-path/concrete-sum/concrete-sum-unsafe.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int main(void) {
+  unsigned n = 1;
+  unsigned sum = 0;
+
+  while (n <= N)
+  {
+    sum = sum + n;
+    n = n + 1;
+  }
+
+  assert(sum != ((N * (N + 1)) / 2));
+
+  return 0;
+}
diff --git a/regression/symex-shortest-path/concrete-sum/main.c b/regression/symex-shortest-path/concrete-sum/main.c
new file mode 100644
index 0000000..163066e
--- /dev/null
+++ b/regression/symex-shortest-path/concrete-sum/main.c
@@ -0,0 +1,21 @@
+#include <assert.h>
+
+#define N 40000
+
+// conservatively safe for N <= 46340
+int main(void) {
+  unsigned n = 1;
+  unsigned sum = 0;
+
+  while (n <= N)
+  {
+    sum = sum + n;
+    n = n + 1;
+  }
+
+//#ifndef FORCE_BRANCH
+  assert(sum == ((N * (N + 1)) / 2));
+//#endif
+
+  return 0;
+}
diff --git a/regression/symex-shortest-path/concrete-sum/test.desc b/regression/symex-shortest-path/concrete-sum/test.desc
new file mode 100644
index 0000000..9efefbc
--- /dev/null
+++ b/regression/symex-shortest-path/concrete-sum/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/counter-unsafe/main.c b/regression/symex-shortest-path/counter-unsafe/main.c
new file mode 100644
index 0000000..9094590
--- /dev/null
+++ b/regression/symex-shortest-path/counter-unsafe/main.c
@@ -0,0 +1,39 @@
+// Similar to SV-COMP'14 (loops/count_up_down_false.c) except
+// that we use explicit signedness constraints to support
+// benchmarks with tools that are not bit precise.
+
+#include <assert.h>
+
+#define N 10
+#define ENABLE_CPROVER
+
+#ifdef ENABLE_KLEE
+#include <klee/klee.h>
+#endif
+
+#ifdef ENABLE_CPROVER
+int nondet_int();
+#endif
+
+// It suffices to unwind N times
+int main() {
+#ifdef ENABLE_CPROVER
+  int n = nondet_int();
+  __CPROVER_assume(0 <= n && n < N);
+#elif ENABLE_KLEE
+  int n;
+  klee_make_symbolic(&n, sizeof(n), "n");
+  if (0 > n)
+    return 0;
+  if (n >= N)
+    return 0;
+#endif
+
+  int x = n, y = 0;
+  while (x > 0) {
+    x = x - 1;
+    y = y + 1;
+  }
+  assert(0 <= y && y != n);
+  return 0;
+}
diff --git a/regression/symex-shortest-path/counter-unsafe/test.desc b/regression/symex-shortest-path/counter-unsafe/test.desc
new file mode 100644
index 0000000..510460c
--- /dev/null
+++ b/regression/symex-shortest-path/counter-unsafe/test.desc
@@ -0,0 +1,6 @@
+CORE
+main.c
+
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/for-loop/main.c b/regression/symex-shortest-path/for-loop/main.c
new file mode 100644
index 0000000..a3ba7e4
--- /dev/null
+++ b/regression/symex-shortest-path/for-loop/main.c
@@ -0,0 +1,13 @@
+void main()
+{
+  int i,x,y=0,z=0;
+  for(i=0;i < 10;++i)
+  //while(1)
+  {
+    if(x)
+     y++;
+    else
+     z++;
+  }
+  assert(1);
+}
diff --git a/regression/symex-shortest-path/for-loop/test.desc b/regression/symex-shortest-path/for-loop/test.desc
new file mode 100644
index 0000000..9efefbc
--- /dev/null
+++ b/regression/symex-shortest-path/for-loop/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/function_pointer1/main.c b/regression/symex-shortest-path/function_pointer1/main.c
new file mode 100644
index 0000000..debb8e8
--- /dev/null
+++ b/regression/symex-shortest-path/function_pointer1/main.c
@@ -0,0 +1,32 @@
+#include <assert.h>
+
+void (*f_ptr)(void);
+
+int global;
+
+void f1(void)
+{
+  global=1;
+}
+
+void f2(void)
+{
+  global=2;
+}
+
+int main()
+{
+  int input;
+
+  f_ptr=f1;
+  f_ptr();
+//  assert(global==1);
+
+  f_ptr=f2;
+  f_ptr();
+//  assert(global==2);
+
+  f_ptr=input?f1:f2;
+  f_ptr();
+  assert(global==(input?1:2));
+}
diff --git a/regression/symex-shortest-path/function_pointer1/test.desc b/regression/symex-shortest-path/function_pointer1/test.desc
new file mode 100644
index 0000000..9efefbc
--- /dev/null
+++ b/regression/symex-shortest-path/function_pointer1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/insertion-sort-unsafe/main.c b/regression/symex-shortest-path/insertion-sort-unsafe/main.c
new file mode 100644
index 0000000..21960ff
--- /dev/null
+++ b/regression/symex-shortest-path/insertion-sort-unsafe/main.c
@@ -0,0 +1,47 @@
+// This file contains modified code snippets from "Algorithms in C, Third Edition,
+// Parts 1-4," by Robert Sedgewick. The code is intentionally buggy!
+//
+// For the correct code, see https://www.cs.princeton.edu/~rs/Algs3.c1-4/code.txt
+
+#include <assert.h>
+
+#define N 5
+
+
+#ifdef ENABLE_KLEE
+#include <klee/klee.h>
+#endif
+
+typedef int Item;
+#define key(A) (A)
+#define less(A, B) (key(A) < key(B))
+#define exch(A, B) { Item t = A; A = B; B = t; }
+#define compexch(A, B) if (less(B, A)) exch(A, B)
+
+void insertion_sort(Item a[], int l, int r) {
+  int i;
+  for (i = l+1; i <= r; i++) compexch(a[l], a[i]);
+  for (i = l+2; i <= r; i++) {
+    int j = i; Item v = a[i];
+    while (0 < j && less(v, a[j-1])) {
+      a[j] = a[j]; j--;
+      //       ^ bug due to wrong index (it should be j-1)
+    }
+    a[j] = v;
+  }
+}
+
+// To find bug, let N >= 4.
+int main() {
+  int a[N];
+
+#ifdef ENABLE_KLEE
+  klee_make_symbolic(a, sizeof(a), "a");
+#endif
+
+  insertion_sort(a, 0, N-1);
+  for (unsigned i = 0; i < N - 1; i++)
+    assert(a[i] <= a[i+1]);
+
+  return 0;
+}
diff --git a/regression/symex-shortest-path/insertion-sort-unsafe/test.desc b/regression/symex-shortest-path/insertion-sort-unsafe/test.desc
new file mode 100644
index 0000000..510460c
--- /dev/null
+++ b/regression/symex-shortest-path/insertion-sort-unsafe/test.desc
@@ -0,0 +1,6 @@
+CORE
+main.c
+
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/modulus-safe/main.c b/regression/symex-shortest-path/modulus-safe/main.c
new file mode 100644
index 0000000..c2d0d52
--- /dev/null
+++ b/regression/symex-shortest-path/modulus-safe/main.c
@@ -0,0 +1,38 @@
+#include <assert.h>
+
+#define N 20
+
+#define ENABLE_CPROVER
+#ifdef ENABLE_KLEE
+#include <klee/klee.h>
+#endif
+
+#ifdef ENABLE_CPROVER
+int nondet_int();
+#endif
+
+int main(void) {
+#ifdef ENABLE_CPROVER
+  int k = nondet_int();
+  __CPROVER_assume(0 <= k && k < 7);
+#elif ENABLE_KLEE
+  int k;
+  klee_make_symbolic(&k, sizeof(k), "k");
+
+  if (0 > k)
+    return 0;
+  if (k >= 7)
+    return 0;
+#endif
+
+  for(int n = 0; n < N; n = n + 1) {
+    if(k == 7) {
+      k = 0;
+    }
+    k = k + 1;
+  }
+
+#ifndef FORCE_BRANCH
+  assert(k <= 7);
+#endif
+}
diff --git a/regression/symex-shortest-path/modulus-safe/test.desc b/regression/symex-shortest-path/modulus-safe/test.desc
new file mode 100644
index 0000000..9efefbc
--- /dev/null
+++ b/regression/symex-shortest-path/modulus-safe/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/modulus-unsafe/main.c b/regression/symex-shortest-path/modulus-unsafe/main.c
new file mode 100644
index 0000000..ebe9be3
--- /dev/null
+++ b/regression/symex-shortest-path/modulus-unsafe/main.c
@@ -0,0 +1,31 @@
+#include <assert.h>
+
+#define N 20
+
+
+#define ENABLE_CPROVER
+#ifdef ENABLE_KLEE
+#include <klee/klee.h>
+#endif
+
+#ifdef ENABLE_CPROVER
+int nondet_int();
+#endif
+
+int main(void) {
+#ifdef ENABLE_CPROVER
+  int k = nondet_int();
+#elif ENABLE_KLEE
+  int k;
+  klee_make_symbolic(&k, sizeof(k), "k");
+#endif
+
+  for(int n = 0; n < N; n = n + 1) {
+    if(k == 7) {
+      k = 0;
+    }
+    k = k + 1;
+  }
+
+  assert(k <= 7);
+}
diff --git a/regression/symex-shortest-path/modulus-unsafe/test.desc b/regression/symex-shortest-path/modulus-unsafe/test.desc
new file mode 100644
index 0000000..510460c
--- /dev/null
+++ b/regression/symex-shortest-path/modulus-unsafe/test.desc
@@ -0,0 +1,6 @@
+CORE
+main.c
+
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/pointer2/main.c b/regression/symex-shortest-path/pointer2/main.c
new file mode 100644
index 0000000..bc6f95a
--- /dev/null
+++ b/regression/symex-shortest-path/pointer2/main.c
@@ -0,0 +1,31 @@
+#include <assert.h>
+
+struct S1
+{
+  char ch0, ch1, ch2, ch3;
+} my_struct1;
+
+struct S2
+{
+  int i1, i2;
+} my_struct2;
+
+int main()
+{
+  // a pointer into a struct
+  int *p=(int *)&my_struct1;
+
+  *p=0x03020100;
+
+  // endianness-dependent
+ // assert(my_struct1.ch0==0);
+ // assert(my_struct1.ch1==1);
+ // assert(my_struct1.ch2==2);
+ // assert(my_struct1.ch3==3);
+
+  // same bigger
+  long long int *q=(long long int *)&my_struct2;
+  *q=0x200000001ull;
+//  assert(my_struct2.i1==1);
+  assert(my_struct2.i2==2);
+}
diff --git a/regression/symex-shortest-path/pointer2/test.desc b/regression/symex-shortest-path/pointer2/test.desc
new file mode 100644
index 0000000..9845e70
--- /dev/null
+++ b/regression/symex-shortest-path/pointer2/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--little-endian
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/pointer3/main.c b/regression/symex-shortest-path/pointer3/main.c
new file mode 100644
index 0000000..65ef310
--- /dev/null
+++ b/regression/symex-shortest-path/pointer3/main.c
@@ -0,0 +1,14 @@
+#include <assert.h>
+
+int main()
+{
+  int choice;
+  int x=1, y=2, *p=choice?&x:&y;
+
+  *p=3;
+
+  if(choice)
+    assert(x==3 && y==2);
+//  else
+  //  assert(x==1 && y==3);
+}
diff --git a/regression/symex-shortest-path/pointer3/test.desc b/regression/symex-shortest-path/pointer3/test.desc
new file mode 100644
index 0000000..9845e70
--- /dev/null
+++ b/regression/symex-shortest-path/pointer3/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--little-endian
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/show-trace1/main.c b/regression/symex-shortest-path/show-trace1/main.c
new file mode 100644
index 0000000..3b21655
--- /dev/null
+++ b/regression/symex-shortest-path/show-trace1/main.c
@@ -0,0 +1,15 @@
+int input();
+
+int main()
+{
+  int i, j, k;
+
+  i=input(); // expect 2
+  j=input(); // expect 3
+  k=input(); // expect 6
+
+  if(i==2)
+    if(j==i+1)
+      if(k==i*j)
+        __CPROVER_assert(0, "");
+}
diff --git a/regression/symex-shortest-path/show-trace1/test.desc b/regression/symex-shortest-path/show-trace1/test.desc
new file mode 100644
index 0000000..930f344
--- /dev/null
+++ b/regression/symex-shortest-path/show-trace1/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--trace
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^  i=2 .*$
+^  j=3 .*$
+^  k=6 .*$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/stop-on-fail1/main.c b/regression/symex-shortest-path/stop-on-fail1/main.c
new file mode 100644
index 0000000..4c51c77
--- /dev/null
+++ b/regression/symex-shortest-path/stop-on-fail1/main.c
@@ -0,0 +1,12 @@
+#include <assert.h>
+
+int main()
+{
+  assert(0);
+  unsigned count=0;
+  while(count!=10)
+  {
+    // merry go around
+  }
+
+}
diff --git a/regression/symex-shortest-path/stop-on-fail1/test.desc b/regression/symex-shortest-path/stop-on-fail1/test.desc
new file mode 100644
index 0000000..fef4ac2
--- /dev/null
+++ b/regression/symex-shortest-path/stop-on-fail1/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--stop-on-fail
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\[main.assertion.1\] assertion 0: FAILURE$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/struct1/main.c b/regression/symex-shortest-path/struct1/main.c
new file mode 100644
index 0000000..3664bd6
--- /dev/null
+++ b/regression/symex-shortest-path/struct1/main.c
@@ -0,0 +1,25 @@
+#include <assert.h>
+
+struct inner_struct
+{
+  int a, b, c;
+};
+
+struct top_level
+{
+  int x, y, z;
+  struct inner_struct inner;
+};
+
+struct top_level my_s = { 1, 2, 3, 4, 5, 6 };
+struct inner_struct my_inner;
+
+int main()
+{
+//  assert(my_s.inner.a==4);
+//  assert(my_inner.a==0);
+  my_inner.a++;
+//  assert(my_inner.a==1);
+  my_s.inner=my_inner; // assigns all of 'inner'
+  assert(my_s.inner.a==1);
+}
diff --git a/regression/symex-shortest-path/struct1/test.desc b/regression/symex-shortest-path/struct1/test.desc
new file mode 100644
index 0000000..9efefbc
--- /dev/null
+++ b/regression/symex-shortest-path/struct1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/struct2/main.c b/regression/symex-shortest-path/struct2/main.c
new file mode 100644
index 0000000..a0781a6
--- /dev/null
+++ b/regression/symex-shortest-path/struct2/main.c
@@ -0,0 +1,18 @@
+#include <assert.h>
+
+struct X
+{
+  int a, b;
+} x;
+
+int main()
+{
+  int *p;
+
+  p=&x.a;
+  *p=10;
+  p++;
+  *p=11;
+
+  assert(x.a==10 && x.b==11);
+}
diff --git a/regression/symex-shortest-path/struct2/test.desc b/regression/symex-shortest-path/struct2/test.desc
new file mode 100644
index 0000000..9efefbc
--- /dev/null
+++ b/regression/symex-shortest-path/struct2/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/struct3/main.c b/regression/symex-shortest-path/struct3/main.c
new file mode 100644
index 0000000..c4363dc
--- /dev/null
+++ b/regression/symex-shortest-path/struct3/main.c
@@ -0,0 +1,37 @@
+#include <assert.h>
+
+struct S
+{
+  char a, b, c, d;
+} x, y;
+
+int main()
+{
+  int i;
+  char *p;
+
+  p=&x.a;
+
+  p[0]=1;
+  p[1]=2;
+  p[2]=3;
+  p[3]=4;
+
+//  assert(x.a==1);
+//  assert(x.b==2);
+//  assert(x.c==3);
+//  assert(x.d==4);
+
+  // same again, directly to head of struct
+  p=(char *)&y;
+
+  p[0]=1;
+  p[1]=2;
+  p[2]=3;
+  p[3]=4;
+
+//  assert(y.a==1);
+//  assert(y.b==2);
+//  assert(y.c==3);
+  assert(y.d==4);
+}
diff --git a/regression/symex-shortest-path/struct3/test.desc b/regression/symex-shortest-path/struct3/test.desc
new file mode 100644
index 0000000..9efefbc
--- /dev/null
+++ b/regression/symex-shortest-path/struct3/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/tp1/main.c b/regression/symex-shortest-path/tp1/main.c
new file mode 100644
index 0000000..944569e
--- /dev/null
+++ b/regression/symex-shortest-path/tp1/main.c
@@ -0,0 +1,127 @@
+struct state_element_f{
+	unsigned int x; // Mode Variable
+	unsigned int diff;
+	unsigned int add;
+};
+
+unsigned int f(unsigned int t, struct state_element_f stf)
+{
+	unsigned int m1;
+	if(t>=1 && t<=5) {
+		//t=1; //extra logic
+		stf.diff=1;
+		m1=1;
+	}
+	else if(t>5 && t<=10){
+		//t=2; //extra logic
+		stf.add=1;
+	        m1=0;
+	}
+	else if(t > 11 && t <= 20 ){
+		t=3; //extra logic
+		stf.add=0;
+	        m1=1;
+	}
+  else { }
+  return t;
+}
+
+struct state_element_g{
+	unsigned int y; // Mode Variable
+	unsigned int avg;
+	unsigned int sum;
+};
+
+void g(unsigned int z, struct state_element_g stg)
+{
+	unsigned int m2;
+	if(z >=1 && z <= 5) {
+		//z=1; //extra logic
+		stg.avg=1;
+		m2++;
+	}
+	else if(z>5 && z<=10){
+		//z=2; //extra logic
+		stg.sum=1;
+		m2--;
+
+		// redundant logic
+		if(m2==1)
+			m2*=2;
+		else
+			m2/=2;
+	}
+	else if(z>11 && z <= 20) {
+		z=3; //extra logic
+	        stg.sum=0;
+	}
+	//**********
+	else {}
+	//**********
+}
+
+void main()
+{
+	//*******************************************************
+	// Total Paths = 19, Feasible Path=3, Infeasible Path=16
+	// ******************************************************
+
+	unsigned int m,n;
+  // Structures are passed as function arguments to build the harness
+  struct state_element_f stf;
+  struct state_element_g stg;
+	//__CPROVER_assume(0);
+	// Identify and bind equivalent signals in both design to allow partitioning
+	/*if(nondet_bool())
+	{
+	  m=1;
+	  n=1;
+	}
+	else if(nondet_bool())
+	{
+		m=2;
+		n=2;
+	}
+	else if(nondet_bool())
+	{
+	  m=3;
+		n=3;
+	}
+	else {
+	  __CPROVER_assume(m==n);
+	}*/
+//	__CPROVER_assume(m==n);
+        m=nondet_unsigned();
+	n=f(m,stf);
+	//n=m;
+	g(n,stg);
+	assert(1);
+  //****************************************************
+
+ 	//*****************************************************
+	// Total Paths = 16, Feasible Path=16, Infeasible Path=0
+	// ****************************************************
+	/*unsigned int m;
+  // Structures are passed as function arguments to build the harness
+  struct state_element_f stf;
+  struct state_element_g stg;
+	f(m,stf);
+	g(m,stg);
+	assert(1);*/
+  //****************************************************
+
+  //*****************************************************************************
+	// When the last else of g() contains the extra code of if-else statement, then
+	// Total Paths = 44, Feasible Path=1, Infeasible Path=43
+	// ****************************************************************************
+	/*unsigned int m;
+  // Structures are passed as function arguments to build the harness
+  struct state_element_f stf;
+  struct state_element_g stg;
+	// Identify and bind equivalent signals in both design to allow partitioning
+	__CPROVER_assume(stf.x == 1 && stg.y == 1);
+	f(m,stf);
+	g(m,stg);
+	assert(1);*/
+  //****************************************************
+}
diff --git a/regression/symex-shortest-path/tp1/test.desc b/regression/symex-shortest-path/tp1/test.desc
new file mode 100644
index 0000000..9efefbc
--- /dev/null
+++ b/regression/symex-shortest-path/tp1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/tp2/main.c b/regression/symex-shortest-path/tp2/main.c
new file mode 100644
index 0000000..141cbde
--- /dev/null
+++ b/regression/symex-shortest-path/tp2/main.c
@@ -0,0 +1,57 @@
+struct state_element_f{
+	unsigned int x;
+	unsigned int diff;
+	unsigned int add;
+};
+
+unsigned int f(unsigned int t, struct state_element_f stf)
+{
+	unsigned int m1;
+	if(t>1) {
+                stf.x=1;
+		stf.diff=1;
+		m1=1;
+	}
+	else {
+		stf.add=1;
+	  m1=0;
+	}
+  return t;
+}
+
+struct state_element_g{
+	unsigned int y;
+	unsigned int avg;
+	unsigned int sum;
+};
+
+void g(unsigned int k, struct state_element_g stg)
+{
+	unsigned int m2;
+	if(k>1) {
+		stg.y=1;
+		stg.avg=1;
+		m2++;
+	}
+	else {
+		stg.sum=1;
+		m2--;
+	}
+}
+
+void main()
+{
+	//*****************************************************
+	// Total Paths = 2, Feasible Path=2, Infeasible Path=0
+	// ****************************************************
+	unsigned int m, n;
+  // Structures are passed as function arguments to build the harness
+  struct state_element_f stf;
+  struct state_element_g stg;
+	// Identify and bind equivalent signals in both design to allow partitioning
+	m=nondet_unsigned();
+	n=f(m,stf);
+	g(n,stg);
+	assert(1);
+  //****************************************************
+}
diff --git a/regression/symex-shortest-path/tp2/test.desc b/regression/symex-shortest-path/tp2/test.desc
new file mode 100644
index 0000000..9efefbc
--- /dev/null
+++ b/regression/symex-shortest-path/tp2/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/tp3/main.c b/regression/symex-shortest-path/tp3/main.c
new file mode 100644
index 0000000..3019b11
--- /dev/null
+++ b/regression/symex-shortest-path/tp3/main.c
@@ -0,0 +1,129 @@
+struct state_element_f{
+	unsigned int x; // Mode Variable
+	unsigned int diff;
+	unsigned int add;
+};
+
+unsigned int f(unsigned int t, struct state_element_f stf)
+{
+	unsigned int m1;
+	if(t==1) {
+		//t=1; //extra logic
+		stf.diff=1;
+		m1=1;
+	}
+	else if(t==2){
+		//t=2; //extra logic
+		stf.add=1;
+	  m1=0;
+	}
+	else if(t==3){
+		//t=3; //extra logic
+		stf.add=0;
+	  m1=1;
+	}
+  else { }; //t= 4; }
+  return t;
+}
+
+struct state_element_g{
+	unsigned int y; // Mode Variable
+	unsigned int avg;
+	unsigned int sum;
+};
+
+void g(unsigned int z, struct state_element_g stg)
+{
+	unsigned int m2;
+	if(z==1) {
+		z=1; //extra logic
+		stg.avg=1;
+		m2++;
+	}
+	else if(z==2){
+		z=2; //extra logic
+		stg.sum=1;
+		m2--;
+
+		// redundant logic
+		if(m2==1)
+			m2*=2;
+		else
+			m2/=2;
+	}
+	else if(z==3) {
+		z=3; //extra logic
+	  stg.sum=0;
+	}
+	//**********
+	else {
+          z = 4;
+        }
+	//**********
+}
+
+void main()
+{
+	//*******************************************************
+	// Total Paths = 19, Feasible Path=3, Infeasible Path=16
+	// ******************************************************
+
+	unsigned int m,n;
+  // Structures are passed as function arguments to build the harness
+  struct state_element_f stf;
+  struct state_element_g stg;
+	//__CPROVER_assume(0);
+	// Identify and bind equivalent signals in both design to allow partitioning
+	/*if(nondet_bool())
+	{
+	  m=1;
+	  n=1;
+	}
+	else if(nondet_bool())
+	{
+		m=2;
+		n=2;
+	}
+	else if(nondet_bool())
+	{
+	  m=3;
+		n=3;
+	}
+	else {
+	  __CPROVER_assume(m==n);
+	}*/
+//	__CPROVER_assume(m==n);
+        m=nondet_unsigned();
+	n=f(m,stf);
+	//n=m;
+	g(n,stg);
+	assert(1);
+  //****************************************************
+
+ 	//*****************************************************
+	// Total Paths = 16, Feasible Path=16, Infeasible Path=0
+	// ****************************************************
+	/*unsigned int m;
+  // Structures are passed as function arguments to build the harness
+  struct state_element_f stf;
+  struct state_element_g stg;
+	f(m,stf);
+	g(m,stg);
+	assert(1);*/
+  //****************************************************
+
+  //*****************************************************************************
+	// When the last else of g() contains the extra code of if-else statement, then
+	// Total Paths = 44, Feasible Path=1, Infeasible Path=43
+	// ****************************************************************************
+	/*unsigned int m;
+  // Structures are passed as function arguments to build the harness
+  struct state_element_f stf;
+  struct state_element_g stg;
+	// Identify and bind equivalent signals in both design to allow partitioning
+	__CPROVER_assume(stf.x == 1 && stg.y == 1);
+	f(m,stf);
+	g(m,stg);
+	assert(1);*/
+  //****************************************************
+}
diff --git a/regression/symex-shortest-path/tp3/test.desc b/regression/symex-shortest-path/tp3/test.desc
new file mode 100644
index 0000000..9efefbc
--- /dev/null
+++ b/regression/symex-shortest-path/tp3/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/tp4/main.c b/regression/symex-shortest-path/tp4/main.c
new file mode 100644
index 0000000..f41600d
--- /dev/null
+++ b/regression/symex-shortest-path/tp4/main.c
@@ -0,0 +1,60 @@
+struct state_element_f{
+	unsigned int x;
+	unsigned int diff;
+	unsigned int add;
+};
+
+unsigned int f(unsigned int t, struct state_element_f stf)
+{
+	unsigned int m1;
+	if(t==1) {
+		//t=1;
+		stf.x=1;
+		stf.diff=1;
+		m1=1;
+	}
+	else {
+	        //t=2;
+		stf.add=1;
+	  m1=0;
+	}
+  return t;
+}
+
+struct state_element_g{
+	unsigned int y;
+	unsigned int avg;
+	unsigned int sum;
+};
+
+void g(unsigned int k, struct state_element_g stg)
+{
+	unsigned int m2;
+	if(k==1) {
+		stg.y=1;
+		stg.avg=1;
+		m2++;
+	}
+	else {
+		stg.sum=1;
+		m2--;
+	}
+}
+
+void main()
+{
+	//*****************************************************
+	// Total Paths = 2, Feasible Path=2, Infeasible Path=0
+	// ****************************************************
+	unsigned int m, n;
+  // Structures are passed as function arguments to build the harness
+  struct state_element_f stf;
+  struct state_element_g stg;
+	// Identify and bind equivalent signals in both design to allow partitioning
+	m=nondet_unsigned();
+        //__CPROVER_assume(m==n);
+	n=f(m,stf);
+	g(n,stg);
+	assert(1);
+  //****************************************************
+}
diff --git a/regression/symex-shortest-path/tp4/test.desc b/regression/symex-shortest-path/tp4/test.desc
new file mode 100644
index 0000000..9efefbc
--- /dev/null
+++ b/regression/symex-shortest-path/tp4/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/va_args_1/main.c b/regression/symex-shortest-path/va_args_1/main.c
new file mode 100644
index 0000000..d877803
--- /dev/null
+++ b/regression/symex-shortest-path/va_args_1/main.c
@@ -0,0 +1,37 @@
+#include <stdio.h> 
+#include <stdarg.h> 
+#include <assert.h> 
+
+int max(int n, ...);
+
+int main ()
+{
+  int m;
+
+  int y = 7;
+  int u = 2;
+  m = max(3, y, u, 9);
+
+  assert(m == 9);
+
+  return 0;
+}
+
+int max(int n, ...)
+{
+  int i,val,largest;
+
+  va_list vl;
+
+  va_start(vl,n);
+  largest=va_arg(vl,int);
+
+  for (i=1;i<n;i++)
+  {
+    val=va_arg(vl,int);
+    largest=(largest>val)?largest:val;
+  }
+ 
+  va_end(vl);
+  return largest;
+}
diff --git a/regression/symex-shortest-path/va_args_1/test.desc b/regression/symex-shortest-path/va_args_1/test.desc
new file mode 100644
index 0000000..9efefbc
--- /dev/null
+++ b/regression/symex-shortest-path/va_args_1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/va_args_10/main.c b/regression/symex-shortest-path/va_args_10/main.c
new file mode 100644
index 0000000..554187f
--- /dev/null
+++ b/regression/symex-shortest-path/va_args_10/main.c
@@ -0,0 +1,41 @@
+#include <stdio.h> 
+#include <stdarg.h> 
+#include <assert.h> 
+
+int max(int n, ...);
+
+int main ()
+{
+  int m;
+  int m2;
+  int m3;
+
+  m = max(3, 2, 6, 9);
+  
+  m2 = max(3, 4, 11, 1);
+
+  m3 = max(2, m, m2);
+
+  assert(m3 == 6);
+
+  return 0;
+}
+
+int max(int n, ...)
+{
+  int i,val,largest;
+
+  va_list vl;
+
+  va_start(vl,n);
+  largest=va_arg(vl,int);
+
+  for (i=1;i<n;i++)
+  {
+    val=va_arg(vl,int);
+    largest=(largest>val)?largest:val;
+  }
+ 
+  va_end(vl);
+  return largest;
+}
diff --git a/regression/symex-shortest-path/va_args_10/test.desc b/regression/symex-shortest-path/va_args_10/test.desc
new file mode 100644
index 0000000..6de7955
--- /dev/null
+++ b/regression/symex-shortest-path/va_args_10/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/va_args_11/main.c b/regression/symex-shortest-path/va_args_11/main.c
new file mode 100644
index 0000000..d9e0b81
--- /dev/null
+++ b/regression/symex-shortest-path/va_args_11/main.c
@@ -0,0 +1,29 @@
+#include <stdio.h> 
+#include <stdarg.h> 
+#include <assert.h> 
+
+void foo(int n, ...);
+
+int main()
+{
+  foo(1, 1u);
+  foo(2, 2l);
+  foo(3, 3.0);
+  return 0;
+}
+
+void foo(int n, ...)
+{
+  va_list vl;
+
+  va_start(vl,n);
+  
+  switch(n)
+  {
+  case 1: assert(va_arg(vl, unsigned)==1); break;
+  case 2: break;
+  case 3:  break;
+  }
+  
+  va_end(vl);
+}
diff --git a/regression/symex-shortest-path/va_args_11/test.desc b/regression/symex-shortest-path/va_args_11/test.desc
new file mode 100644
index 0000000..9efefbc
--- /dev/null
+++ b/regression/symex-shortest-path/va_args_11/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/va_args_2/main.c b/regression/symex-shortest-path/va_args_2/main.c
new file mode 100644
index 0000000..2a35ca4
--- /dev/null
+++ b/regression/symex-shortest-path/va_args_2/main.c
@@ -0,0 +1,35 @@
+#include <stdio.h> 
+#include <stdarg.h> 
+#include <assert.h> 
+
+int max(int n, ...);
+
+int main ()
+{
+  int m;
+  int y;
+  m = max(2, y, 8);
+
+  assert(m == 8);
+
+  return 0;
+}
+
+int max(int n, ...)
+{
+  int i,val,largest;
+
+  va_list vl;
+
+  va_start(vl,n);
+  largest=va_arg(vl,int);
+
+  for (i=1;i<n;i++)
+  {
+    val=va_arg(vl,int);
+    largest=(largest>val)?largest:val;
+  }
+ 
+  va_end(vl);
+  return largest;
+}
diff --git a/regression/symex-shortest-path/va_args_2/test.desc b/regression/symex-shortest-path/va_args_2/test.desc
new file mode 100644
index 0000000..6de7955
--- /dev/null
+++ b/regression/symex-shortest-path/va_args_2/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/va_args_3/main.c b/regression/symex-shortest-path/va_args_3/main.c
new file mode 100644
index 0000000..148d705
--- /dev/null
+++ b/regression/symex-shortest-path/va_args_3/main.c
@@ -0,0 +1,34 @@
+#include <stdio.h> 
+#include <stdarg.h> 
+#include <assert.h> 
+
+int max(int n, ...);
+
+int main ()
+{
+  int m;
+  m = max(2, 1, 8);
+
+  assert(m == 1);
+
+  return 0;
+}
+
+int max(int n, ...)
+{
+  int i,val,largest;
+
+  va_list vl;
+
+  va_start(vl,n);
+  largest=va_arg(vl,int);
+
+  for (i=1;i<n;i++)
+  {
+    val=va_arg(vl,int);
+    largest=(largest>val)?largest:val;
+  }
+ 
+ 	va_end(vl);
+  return largest;
+}
diff --git a/regression/symex-shortest-path/va_args_3/test.desc b/regression/symex-shortest-path/va_args_3/test.desc
new file mode 100644
index 0000000..6de7955
--- /dev/null
+++ b/regression/symex-shortest-path/va_args_3/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/va_args_4/main.c b/regression/symex-shortest-path/va_args_4/main.c
new file mode 100644
index 0000000..4a19acf
--- /dev/null
+++ b/regression/symex-shortest-path/va_args_4/main.c
@@ -0,0 +1,38 @@
+#include <stdio.h> 
+#include <stdarg.h> 
+#include <assert.h> 
+
+int max(int n, ...);
+
+int main()
+{
+  int m;
+  m = max(2, 2, 8, 10);
+
+  assert(m == 10);
+
+  return 0;
+}
+
+int max(int repeat,int n, ...)
+{
+  int i,val,largest;
+
+  va_list vl;
+
+  va_start(vl,n);
+  largest=va_arg(vl,int);
+
+  for (i=1;i<n;i++)
+  {
+    val=va_arg(vl,int);
+    largest=(largest>val)?largest:val;
+  }
+ 
+  for (i = 0; i < repeat; i++){
+	  printf("%d. Result is: %d", i, largest);	
+  }
+
+ 	va_end(vl);
+  return largest;
+}
diff --git a/regression/symex-shortest-path/va_args_4/test.desc b/regression/symex-shortest-path/va_args_4/test.desc
new file mode 100644
index 0000000..9efefbc
--- /dev/null
+++ b/regression/symex-shortest-path/va_args_4/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/va_args_5/main.c b/regression/symex-shortest-path/va_args_5/main.c
new file mode 100644
index 0000000..a1e4d6a
--- /dev/null
+++ b/regression/symex-shortest-path/va_args_5/main.c
@@ -0,0 +1,35 @@
+#include <stdio.h> 
+#include <stdarg.h> 
+#include <assert.h> 
+
+int max(int n, ...);
+
+int main ()
+{
+  int n;
+  int m;
+  m = max(7, 7, 8);
+
+  assert(m == 8);
+
+  return 0;
+}
+
+int max(int n, ...)
+{
+  int i,val,largest;
+
+  va_list vl;
+
+  va_start(vl,n);
+  largest=va_arg(vl,int);
+
+  for (i=1;i<n;i++)
+  {
+    val=va_arg(vl,int);
+    largest=(largest>val)?largest:val;
+  }
+
+ 	va_end(vl);
+  return largest;
+}
diff --git a/regression/symex-shortest-path/va_args_5/test.desc b/regression/symex-shortest-path/va_args_5/test.desc
new file mode 100644
index 0000000..b69d21c
--- /dev/null
+++ b/regression/symex-shortest-path/va_args_5/test.desc
@@ -0,0 +1,6 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
diff --git a/regression/symex-shortest-path/va_args_6/main.c b/regression/symex-shortest-path/va_args_6/main.c
new file mode 100644
index 0000000..191435f
--- /dev/null
+++ b/regression/symex-shortest-path/va_args_6/main.c
@@ -0,0 +1,34 @@
+#include <stdio.h> 
+#include <stdarg.h> 
+#include <assert.h> 
+
+int max(int n, ...);
+
+int main ()
+{
+  int m;
+  m = max(8, 2, 7, 8);
+
+	assert(m == 2);
+
+	return 0;
+}
+
+int max (int j, int n, ...)
+{
+  int i,val,largest;
+
+  va_list vl;
+
+  va_start(vl,n);
+  largest=va_arg(vl,int);
+
+	for (i=1;i<j;i++)
+  {
+    val=va_arg(vl,int);
+    largest=(largest>val)?largest:val;
+  }
+
+  va_end(vl);
+  return largest;
+}
diff --git a/regression/symex-shortest-path/va_args_6/test.desc b/regression/symex-shortest-path/va_args_6/test.desc
new file mode 100644
index 0000000..9431f04
--- /dev/null
+++ b/regression/symex-shortest-path/va_args_6/test.desc
@@ -0,0 +1,6 @@
+CORE
+main.c
+--unwind 8
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
diff --git a/regression/symex-shortest-path/va_args_7/main.c b/regression/symex-shortest-path/va_args_7/main.c
new file mode 100644
index 0000000..cecc1bf
--- /dev/null
+++ b/regression/symex-shortest-path/va_args_7/main.c
@@ -0,0 +1,23 @@
+#include <stdio.h> 
+#include <stdarg.h> 
+#include <assert.h> 
+
+int main ()
+{
+    
+  int eva_arguments;
+  int n;
+
+  int init_eva = eva_arguments;
+
+  for (unsigned int i = 0; i < n; i++){
+  
+    eva_arguments++;  
+  }
+
+  if (init_eva == 0){
+    assert(eva_arguments == n);  
+  }
+
+  return 0;
+}
diff --git a/regression/symex-shortest-path/va_args_7/test.desc b/regression/symex-shortest-path/va_args_7/test.desc
new file mode 100644
index 0000000..832e94e
--- /dev/null
+++ b/regression/symex-shortest-path/va_args_7/test.desc
@@ -0,0 +1,6 @@
+CORE
+main.c
+--unwind 8
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/symex-shortest-path/va_args_8/main.c b/regression/symex-shortest-path/va_args_8/main.c
new file mode 100644
index 0000000..90e2031
--- /dev/null
+++ b/regression/symex-shortest-path/va_args_8/main.c
@@ -0,0 +1,37 @@
+#include <stdio.h> 
+#include <stdarg.h> 
+#include <assert.h> 
+
+int max(int n, ...);
+
+int main ()
+{
+  int m;
+
+  int y = 7;
+  int u = 2;
+  m = max(3, y, u, 9);
+
+  assert(m == 10);
+
+  return 0;
+}
+
+int max(int n, ...)
+{
+  int i,val,largest;
+
+  va_list vl;
+
+  va_start(vl,n);
+  largest=va_arg(vl,int) + 1;
+
+  for (i=1;i<n;i++)
+  {
+    val=va_arg(vl,int) + 1;
+    largest=(largest>val)?largest:val;
+  }
+ 
+  va_end(vl);
+  return largest;
+}
diff --git a/regression/symex-shortest-path/va_args_8/test.desc b/regression/symex-shortest-path/va_args_8/test.desc
new file mode 100644
index 0000000..9efefbc
--- /dev/null
+++ b/regression/symex-shortest-path/va_args_8/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-shortest-path/va_args_9/main.c b/regression/symex-shortest-path/va_args_9/main.c
new file mode 100644
index 0000000..4c9d52b
--- /dev/null
+++ b/regression/symex-shortest-path/va_args_9/main.c
@@ -0,0 +1,41 @@
+#include <stdio.h> 
+#include <stdarg.h> 
+#include <assert.h> 
+
+int max(int n, ...);
+
+int main ()
+{
+  int m;
+  int m2;
+  int m3;
+
+  m = max(3, 2, 6, 9);
+  m2 = max(3, 4, 11, 1);
+
+  m3 = max(2, m, m2);
+
+  assert(m3 == 11);
+
+  return 0;
+}
+
+int max(int n, ...)
+{
+  int i,val,largest;
+
+  va_list vl;
+
+  va_start(vl,n);
+  largest=va_arg(vl,int);
+
+  for (i=1;i<n;i++)
+  {
+    val=va_arg(vl,int);
+    largest=(largest>val)?largest:val;
+  }
+ 
+  va_end(vl);
+
+  return largest;
+}
diff --git a/regression/symex-shortest-path/va_args_9/test.desc b/regression/symex-shortest-path/va_args_9/test.desc
new file mode 100644
index 0000000..9efefbc
--- /dev/null
+++ b/regression/symex-shortest-path/va_args_9/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

From e2daa85f394da2d088d278ac8e76dfe86afa2121 Mon Sep 17 00:00:00 2001
From: polgreen <elizabeth.polgreen@cs.ox.ac.uk>
Date: Tue, 14 Nov 2017 10:30:13 +0000
Subject: [PATCH 12/12] makefile for regression tests

---
 regression/symex-shortest-path/Makefile | 21 +++++++++++++++++----
 1 file changed, 17 insertions(+), 4 deletions(-)

diff --git a/regression/symex-shortest-path/Makefile b/regression/symex-shortest-path/Makefile
index c21125c..3285ad6 100644
--- a/regression/symex-shortest-path/Makefile
+++ b/regression/symex-shortest-path/Makefile
@@ -1,13 +1,26 @@
 default: tests.log
 
 test:
-	@../test.pl -c "../../../src/symex/symex --shortest-path"
-	@../test.pl -c "../../../src/symex/symex --shortest-path --randomize"
+	@if ! ../../lib/cbmc/regression/test.pl -c "../../../src/symex/symex --shortest-path" ; then \
+		../../lib/cbmc/regression/failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+		@if ! ../../lib/cbmc/regression/test.pl -c "../../../src/symex/symex --shortest-path --randomize" ; then \
+		../../lib/cbmc/regression/failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
 
 tests.log: ../test.pl
-	@../test.pl -c "../../../src/symex/symex --shortest-path"
-	@../test.pl -c "../../../src/symex/symex --shortest-path --randomize"
+	@if ! ../../lib/cbmc/regression/test.pl -c "../../../src/symex/symex --shortest-path" ; then \
+		../../lib/cbmc/regression/failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
 
+	@if ! ../../lib/cbmc/regression/test.pl -c ../../../src/symex/symex "--shortest-path --randomize" ; then \
+		../../lib/cbmc/regression/failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
 
 show:
 	@for dir in *; do \