From f435f50c48789f442ffb27cdb90578e241f17659 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 11 Feb 2020 11:11:30 -0800
Subject: Different heuristic

---
 src/theory/strings/core_solver.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 18dd0bb3c..f30691e0c 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -1189,7 +1189,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
 
     // The candidate inference "info"
     InferInfo info;
-    info.d_index = index;
+    info.d_index = std::max(x.getId(), y.getId());
     // for debugging
     info.d_i = nfi.d_base;
     info.d_j = nfj.d_base;
-- 
cgit v1.2.3