Only store projection equate for solved goals

cognitive-engineering-lab · Aug 27, 2024 · b7727c4 · b7727c4
1 parent 3528b1e
commit b7727c4
Showing 1 changed file with 6 additions and 5 deletions.
diff --git a/crates/argus/src/proof_tree/serialize.rs b/crates/argus/src/proof_tree/serialize.rs
@@ -50,11 +50,12 @@ impl SerializedTreeVisitor<'_> {
   }
 
   fn check_goal_projection(&mut self, goal: &InspectGoal) {
-    if let ty::PredicateKind::AliasRelate(
-      t1,
-      t2,
-      ty::AliasRelationDirection::Equate,
-    ) = goal.goal().predicate.kind().skip_binder()
+    if goal.result().is_yes()
+      && let ty::PredicateKind::AliasRelate(
+        t1,
+        t2,
+        ty::AliasRelationDirection::Equate,
+      ) = goal.goal().predicate.kind().skip_binder()
       && let Some(mut t1) = t1.ty()
       && let Some(mut t2) = t2.ty()
       // Disallow projections involving two aliases