Commit d6203 breaks PLE?

[shingarov]

Since commit d6203 (Send bindings to the SMT solver ahead of validating constraints), all tests/horn/pos/ple* and tests/horn/neg/ple* tests crash like this:

...
Computing Result
SMT READ
SMT Says: Error "line 126 column 42: invalid named expression, declaration already defined with this name b$36$$35$$35$0"
Crash!: :1:1-1:1: Error
  crash: SMTLIB2 respSat = Error "line 126 column 42: invalid named expression, declaration already defined with this name b$36$$35$$35$0"

Is this intended?

[facundominguez]

Hello!

Is this intended?

It is not intended as far as I'm aware. The following command succeeds for me at d3bcbd0 (develop branch).

$ stack exec fixpoint -- liquid-fixpoint/tests/horn/pos/ple0.smt2

also

stack build --test liquid-fixpoint

I'm running everything from the liquidhaskell repo. But perhaps you have some instructions to reproduce (?)

[shingarov]

I simply do

$ git clone https://github.com/ucsd-progsys/liquid-fixpoint.git
$ cd liquid-fixpoint
$ stack install

Then

fixpoint -v tests/horn/pos/ple0.smt2

gives the above crash.

[shingarov]

But if I checkout any preceding commit, it works just fine:

RESULT: Safe (Stats {numCstr = 1, numIter = 2, numBrkt = 2, numChck = 2, numVald = 1})
Safe ( 1  constraints checked)

[facundominguez]

It works in my local environment, and it works in CI as well:
https://app.circleci.com/pipelines/github/facundominguez/liquid-fixpoint/3/workflows/da6f3530-147b-4041-8c81-425700ad2f87/jobs/3/parallel-runs/0/steps/0-109

I checked the code, and can't see why it would fail as reported.

Still, if someone can reproduce it, please feel free to investigate. Or maybe if @shingarov can make it fail in CI, we could investigate it from there.

[ranjitjhala]

@shingarov -- what version of z3 do you have? I wonder if that is the issue here? [ though its odd that earlier commits are ok ... ]

[ranjitjhala]

Can you tell us the result of z3 --version ?

[shingarov]

$ z3 --version
Z3 version 4.8.9 - 64 bit

[ranjitjhala]

hmm and can you also send over these two files (the ones that are crashing)

• tests/horn/pos/.liquid/ple0.smt2.smt2
• tests/horn/pos/.liquid/ple0.smt2.evals.smt2

[shingarov]

ple0.smt2.evals.smt2.txt
ple0.smt2.smt2.txt

[shingarov]

(sorry had to append .txt to the names because this UI rejects attachments based on "extension")