check_ir_equivalence gets some questions

When my inputs of check_ir_equivalence_main are two same ir files, however get the result: **slover result: satisfiable false**
```
root@DESKTOP-NBI1920:/mnt/g/xls# cat test.ir
package my_package

file_number 1 "./test.c"

top fn test(a: bits[32]) -> bits[32] {
literal.2: bits[32] = literal(value=3, id=2, pos=[(1,5,5)])
ret add.3: bits[32] = add(a, literal.2, id=3, pos=[(1,5,5)])
}

root@DESKTOP-NBI1920:/mnt/g/xls# cat test.opt.ir
package my_package

file_number 1 "./test.c"

top fn test(a: bits[32]) -> bits[32] {
literal.2: bits[32] = literal(value=3, id=2, pos=[(1,5,5)])
ret add.3: bits[32] = add(a, literal.2, id=3, pos=[(1,5,5)])
}

root@DESKTOP-NBI1920:/mnt/g/xls# ./bazel-bin/xls/tools/check_ir_equivalence_main test.ir test.opt.ir
Solver result; satisfiable: false
```