Cryptol generates SMT files that abc can't parse

[jpziegler]

See issue #71 on abc's BitBucket. Apparently Cryptol sometimes generates arrays, which abc can't handle.

I'll post the relevant Cryptol code when I have the chance.

[atomb]

I suspect we could, when using ABC, pre-process the formulas to translate array operations into lower-level constructs. For other solvers, we probably want to leave the arrays in to take advantage of efficient built-in support for them.

[atomb]

Let's see if this is still a problem with What4 (#647). Otherwise it's an SBV-specific issue.

[robdockins]

Seems clear this is a bug, just not sure whose.

[robdockins]

@jpziegler, it's been awhile now, but do you happen to still have the input that generated this bug? I'm not sure how to reproduce.

[weaversa]

@robdockins look no further than your own comment in #573

Cryptol> :s prover=abc
Cryptol> :prove \(r:[5]) (x:[32]) -> (x <<< r) >>> r == x

SBV exception:

*** Data.SBV: fd:15: hGetLine: end of file:
***
***    Sent      : (check-sat)
***
***    Executable: /Users/fett/local/bin/abc
***    Options   : -S "%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000"

The smt file contains the following offending lines:

; --- skolemized tables ---
(declare-fun table0 ((_ BitVec 5)) (_ BitVec 32))
(declare-fun table1 ((_ BitVec 5)) (_ BitVec 32))

[robdockins]

Ah, what a coincidence! That explains that mystery. OK, this seems like an SBV bug then. I'll file an upstream ticket.

[robdockins]

PR #1234 added a w4-abc prover that communicates with ABC as an external process. Using this new prover setting, we can handle the example above.

Cryptol> :set prover=w4-abc
Cryptol> :prove \(r:[5]) (x:[32]) -> (x <<< r) >>> r == x
Q.E.D.
(Total Elapsed Time: 0.059s, using "ABC")

Nobody seems interested in fixing/working around the upstream bug that is causing this, so I think we are going to just close this.