From 9913da25019196ff5898812c41bd9208246c7786 Mon Sep 17 00:00:00 2001
From: Sasha Fedchin <sasha.fedchin@gmail.com>
Date: Mon, 21 Oct 2024 16:20:17 +0200
Subject: [PATCH 1/2] Fix how counterexamples are presented to LanguageServer

---
 .../CounterExampleGeneration/PartialState.cs  | 36 +++++++++++++++++++
 .../Handlers/Custom/CounterExampleItem.cs     |  6 ++--
 .../Custom/DafnyCounterExampleHandler.cs      |  3 +-
 3 files changed, 42 insertions(+), 3 deletions(-)

diff --git a/Source/DafnyCore/CounterExampleGeneration/PartialState.cs b/Source/DafnyCore/CounterExampleGeneration/PartialState.cs
index d16095a5e71..1a89ed7ec14 100644
--- a/Source/DafnyCore/CounterExampleGeneration/PartialState.cs
+++ b/Source/DafnyCore/CounterExampleGeneration/PartialState.cs
@@ -83,6 +83,42 @@ private Expression GetCompactConjunction(List<Expression> conjuncts) {
     return new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, left, right);
   }
 
+  public Dictionary<string, string> AsVariableValueDictionary() {
+    var variableToValue = new Dictionary<PartialValue, Expression>();
+    var variables = ExpandedVariableSet().ToArray();
+    var constraintSet = new HashSet<Constraint>();
+
+    foreach (var variable in variables) {
+      foreach (var constraint in variable.Constraints) {
+        constraintSet.Add(constraint);
+      }
+    }
+
+    Constraint.ResolveAndOrder(variableToValue, constraintSet.ToList(), true, true);
+
+    var variableValuesDictionary = new Dictionary<string, string>();
+    foreach (var variable in variables) {
+      var variableValue = variableToValue[variable].ToString();
+      foreach (var constraint in variable.Constraints.OfType<DefinitionConstraint>()
+                 .Where(constraint => constraint.DefinedValue == variable &&
+                 (constraint is not LiteralExprConstraint) &&
+                 (constraint is not DatatypeValueConstraint) &&
+                 (constraint is not SeqDisplayConstraint))) {
+        if (constraint.ReferencedValues.Any(value => !variableToValue.ContainsKey(value))) {
+          continue;
+        }
+        var variableNameAsExpression = constraint.RightHandSide(variableToValue);
+        var variableNameAsString = variableNameAsExpression.ToString();
+        if (variableValue == variableNameAsString) {
+          continue;
+        }
+        variableValuesDictionary[variableNameAsString] = variableValue + ",";
+      }
+    }
+
+    return variableValuesDictionary;
+  }
+
   /// <summary>
   /// Convert this counterexample state into an assumption that could be inserted in Dafny source code
   /// </summary>
diff --git a/Source/DafnyLanguageServer/Handlers/Custom/CounterExampleItem.cs b/Source/DafnyLanguageServer/Handlers/Custom/CounterExampleItem.cs
index d1aadd9f3bd..6f03ab38e5e 100644
--- a/Source/DafnyLanguageServer/Handlers/Custom/CounterExampleItem.cs
+++ b/Source/DafnyLanguageServer/Handlers/Custom/CounterExampleItem.cs
@@ -4,12 +4,14 @@
 namespace Microsoft.Dafny.LanguageServer.Handlers.Custom {
   public class CounterExampleItem {
     public Position Position { get; }
+    public IDictionary<string, string> Variables { get; }
 
     public string Assumption { get; }
 
-    public CounterExampleItem(Position position, string assumption) {
+    public CounterExampleItem(Position position, IDictionary<string, string> variables, string assumption) {
       Position = position;
+      Variables = variables;
       Assumption = assumption;
     }
   }
-}
+}
\ No newline at end of file
diff --git a/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs b/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs
index 20d70713a81..31638934b75 100644
--- a/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs
+++ b/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs
@@ -109,7 +109,8 @@ private IEnumerable<CounterExampleItem> GetCounterExamples(DafnyModel model) {
       private CounterExampleItem GetCounterExample(PartialState state) {
         return new(
           new Position(state.GetLineId() - 1, state.GetCharId()),
-           state.AsAssumption().ToString()
+           state.AsVariableValueDictionary(),
+          state.AsAssumption().ToString()
          );
       }
     }

From e6dbcd44962fe5692cb6aa1bbd62d34db772a0fd Mon Sep 17 00:00:00 2001
From: Sasha Fedchin <sasha.fedchin@gmail.com>
Date: Mon, 21 Oct 2024 16:25:28 +0200
Subject: [PATCH 2/2] Update docs/dev/news

---
 docs/dev/news/5847.fix | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 docs/dev/news/5847.fix

diff --git a/docs/dev/news/5847.fix b/docs/dev/news/5847.fix
new file mode 100644
index 00000000000..4e31eba55d8
--- /dev/null
+++ b/docs/dev/news/5847.fix
@@ -0,0 +1 @@
+Fixed a bug preventing counterexamples from being displayed in the IDE