Merge branch 'master' of github.com:GaloisInc/pate

tests/integration/packet/packet.exp

@@ -46,7 +46,12 @@ expect "Regenerate result with new trace constraints?"
 expect "0: True"
 send "0\r"
 expect "Waiting for constraints.."
-send "input \"\[ \[ { \\\"var\\\" : { \\\"symbolic_ident\\\" : 0 }, \\\"op\\\" : \\\"EQ\\\", \\\"const\\\" : \\\"128\\\"} \] \]\"\r"
+
+# The identifier here is not stable. Ideally we could fetch it somehow, but if this fails there will be an 
+# 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\\\" : -41624 }, \\\"op\\\" : \\\"EQ\\\", \\\"const\\\" : \\\"128\\\"} \] \]\"\r"
 
 expect "Regenerate result with new trace constraints?"
 expect "1: False"
@@ -68,7 +73,7 @@ expect "0: segment1+0x644 \\\[ via: \"parse_packet\" (segment1+0x554) \\\]"
 expect ">"
 send "0\r"
 
-expect -re {3: let -- segment1\+0x664.. in not v(\d)+}
+expect -re {3: \(Predicate\) let -- segment1\+0x664.. in not v(\d)+}
 expect ">"
 send "3\r"
 
@@ -89,14 +94,11 @@ expect "0: segment1+0x644 \\\[ via: \"parse_packet\" (segment1+0x554) \\\]"
 expect ">"
 send "0\r"
 
-expect -re {0: let -- segment1\+0x664.. in not v(\d)+}
-expect ">"
-send "0\r"
-
-expect "0: Simplified Condition"
-send "0\r"
+expect "5: Simplified Predicate"
+send "5\r"
 
 expect -re {0: let -- segment1\+0x664.. in not v(\d)+}
+expect ">"
 send "0\r"
 
 expect -re {v(\d)+ = eq 0x80:\[8\] \(select \(select cInitMemBytes@(\d)+:a 0\) 0x11045:\[32\]\)}