search

ucsd-progsys / liquid-fixpoint

Horn Clause Constraint Solving for Liquid Types
BSD 3-Clause "New" or "Revised" License
141 stars 61 forks source link

Commit d6203 breaks PLE? #514

Open shingarov opened 3 years ago

shingarov commented 3 years ago

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 commented 3 years ago

Hello!

Is this intended?

It is not intended as far as I'm aware. The following command succeeds for me at d3bcbd0c (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 commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

@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 commented 3 years ago

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

shingarov commented 3 years ago 
$ z3 --version
Z3 version 4.8.9 - 64 bit
ranjitjhala commented 3 years ago

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

shingarov commented 3 years ago

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

shingarov commented 3 years ago

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