de-duplicate memory operations when making a TraceFootprint

src/Pate/Verification/StrongestPosts/CounterExample.hs

@@ -35,6 +35,8 @@ module Pate.Verification.StrongestPosts.CounterExample
 
 import           Data.Text (Text)
 import           Numeric (showHex)
+import qualified Data.Set as Set
+
 
 import qualified Data.Macaw.CFG as MM
 import qualified Data.Macaw.CFGSlice as MCS
@@ -265,14 +267,14 @@ instance (PSo.ValidSym sym, PA.ValidArch arch) => IsTraceNode '(sym,arch) "trace
 
 mkFootprint ::
   forall sym arch.
-  W4.IsExprBuilder sym =>
+  W4.IsSymExprBuilder sym =>
   sym ->
   MT.RegOp sym arch ->
   SymSequence sym (MT.TraceEvent sym arch) -> 
   IO (TraceFootprint sym arch)
 mkFootprint sym init_regs s = do
   init_mems <- W4.concatSymSequence sym go (\_ a b -> return $ a ++ b) (\a b -> return $ a ++ b) [] s
-  return $ TraceFootprint init_regs init_mems
+  return $ TraceFootprint init_regs (Set.toList (Set.fromList init_mems))
   where
     go :: MT.TraceEvent sym arch -> IO [(MM.ArchSegmentOff arch, (MT.MemOp sym (MM.ArchAddrWidth arch)))]
     go = \case

tests/integration/packet/packet.exp

@@ -53,7 +53,7 @@ expect "Waiting for constraints.."
 # error about a missing identifier. The target expression should be the one that ends in 
 # something like: 'select v35113 (bvSum cr5O_offset@34733:bv 0x2:[32]))'
 
-send "input \"\[ \[ { \\\"var\\\" : { \\\"symbolic_ident\\\" : 16893 }, \\\"op\\\" : \\\"EQ\\\", \\\"const\\\" : \\\"128\\\"} \] \]\"\r"
+send "input \"\[ \[ { \\\"var\\\" : { \\\"symbolic_ident\\\" : 17460 }, \\\"op\\\" : \\\"EQ\\\", \\\"const\\\" : \\\"128\\\"} \] \]\"\r"
 
 expect "Regenerate result with new trace constraints?"
 expect "1: False"