diff --git a/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala b/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala index 6717983e38b6e5978f53585295abdcddbeae4d7b..c4373935eadb555a125360fd8055aed5c619a441 100644 --- a/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala +++ b/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala @@ -213,10 +213,10 @@ class ParserTest extends AnyFunSuite with TestUtils { ) assert(Parser.parseSequent("⊢ ('x = 'x) ∨ ('x = 'y)") == (() |- (x === x) \/ (x === y))) assert( - Parser.parseSequent("('x = 'x) ∨ ('x = 'y); ('x = 'x) ∨ ('x = 'y) ↔ ('x = 'x') ∨ ('x = 'y') ⊢ ('x = 'x') ∨ ('x = 'y')") == (Set( + Parser.parseSequent("('x = 'x) ∨ ('x = 'y); ('x = 'x) ∨ ('x = 'y) ↔ ('x = 'x1) ∨ ('x = 'y1) ⊢ ('x = 'x1) ∨ ('x = 'y1)") == (Set( (x === x) \/ (x === y), - ((x === x) \/ (x === y)) <=> ((x === xPrime) \/ (x === yPrime)) - ) |- (x === xPrime) \/ (x === yPrime)) + ((x === x) \/ (x === y)) <=> ((x === x1) \/ (x === y1)) + ) |- (x === x1) \/ (x === y1)) ) } }