Fix unit test build

smowton · Sep 19, 2017 · b544a4b · b544a4b
1 parent 9b8a025
commit b544a4b
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 17 deletions.
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
@@ -42,11 +42,6 @@ static exprt instantiate(
   const string_constraintt &axiom, const exprt &str, const exprt &val);
 static bool is_char_array(const namespacet &ns, const typet &type);
 
-exprt substitute_array_lists(exprt expr, size_t string_max_length);
-
-exprt concretize_arrays_in_expression(
-  exprt expr, std::size_t string_max_length);
-
 static bool is_valid_string_constraint(
   messaget::mstreamt& stream,
   const namespacet& ns,

diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
@@ -96,4 +96,7 @@ class string_refinementt final: public bv_refinementt
 
   void add_lemma(const exprt &lemma, bool simplify=true);
 };
+
+exprt substitute_array_lists(exprt expr, size_t string_max_length);
+exprt concretize_arrays_in_expression(exprt expr, std::size_t string_max_length);
 #endif
diff --git a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
@@ -154,8 +154,7 @@ SCENARIO("instantiate_not_contains",
     symbol_tablet symtab;
     namespacet empty_ns(symtab);
     string_constraint_generatort::infot info;
-    info.ns=&empty_ns;
-    string_constraint_generatort generator(info);
+    string_constraint_generatort generator(info, ns);
     exprt res=generator.add_axioms_for_function_application(func);
     std::string axioms;
     std::vector<string_not_contains_constraintt> nc_axioms;
@@ -242,8 +241,7 @@ SCENARIO("instantiate_not_contains",
     symbol_tablet symtab;
     namespacet empty_ns(symtab);
     string_constraint_generatort::infot info;
-    info.ns=&empty_ns;
-    string_constraint_generatort generator(info);
+    string_constraint_generatort generator(info, ns);
     generator.witness[vacuous]=
       generator.fresh_symbol("w", t.witness_type());
 
@@ -301,8 +299,7 @@ SCENARIO("instantiate_not_contains",
     symbol_tablet symtab;
     namespacet ns(symtab);
     string_constraint_generatort::infot info;
-    info.ns=&ns;
-    string_constraint_generatort generator(info);
+    string_constraint_generatort generator(info, ns);
     generator.witness[trivial]=
       generator.fresh_symbol("w", t.witness_type());
 
@@ -361,8 +358,7 @@ SCENARIO("instantiate_not_contains",
     symbol_tablet symtab;
     namespacet empty_ns(symtab);
     string_constraint_generatort::infot info;
-    info.ns=&empty_ns;
-    string_constraint_generatort generator(info);
+    string_constraint_generatort generator(info, ns);
     generator.witness[trivial]=
       generator.fresh_symbol("w", t.witness_type());
 
@@ -423,8 +419,7 @@ SCENARIO("instantiate_not_contains",
     namespacet empty_ns(symtab);
 
     string_constraint_generatort::infot info;
-    info.ns=&empty_ns;
-    string_constraint_generatort generator(info);
+    string_constraint_generatort generator(info, ns);
     generator.witness[trivial]=
       generator.fresh_symbol("w", t.witness_type());
 
@@ -483,8 +478,7 @@ SCENARIO("instantiate_not_contains",
     symbol_tablet symtab;
     namespacet empty_ns(symtab);
     string_constraint_generatort::infot info;
-    info.ns=&empty_ns;
-    string_constraint_generatort generator(info);
+    string_constraint_generatort generator(info, ns);
     generator.witness[trivial]=
       generator.fresh_symbol("w", t.witness_type());