From 0e5a54e972332ec60e0b6936f3d55495e186dbf4 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 10 Apr 2017 11:03:45 +0100
Subject: [PATCH] Avoid initializing the index set if not needed
 diffblue/test-gen#199

This can improve performances when strings are not important
---
 src/solvers/refinement/string_refinement.cpp | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 23c7ab7f24a..cdd36175296 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -612,6 +612,22 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   found_length.clear();
   found_content.clear();
 
+  // Initial try without index set
+  decision_proceduret::resultt res=supert::dec_solve();
+  if(res==D_SATISFIABLE)
+  {
+    if(!check_axioms())
+    {
+      debug() << "check_SAT: got SAT but the model is not correct" << eom;
+    }
+    else
+    {
+      debug() << "check_SAT: the model is correct" << eom;
+      concretize_lengths();
+      return D_SATISFIABLE;
+    }
+  }
+
   initial_index_set(universal_axioms);
   update_index_set(cur);
   cur.clear();