Open nikivazou opened 2 years ago
I cannot get the reported panic with the latest liquidhaskell
. But I get a different panic now:
$ cabal exec ghc -- -package liquidhaskell Test.hs
...
**** LIQUID: ERROR *************************************************************
<no location info>: error:
Sorry, unexpected panic in liquid-fixpoint!
and liquid-fixpoint
says
$ cabal exec fixpoint -- .liquid/Test.hs.bfq --rewriteaxioms
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California.
All Rights Reserved.
Working 66% [============================================.....................]
Crash!: :1:1-1:1: Error
crash: SMTLIB2 respSat = Error "line 3 column 35747: unknown constant GHC.Err.undefinedReal declared: (declare-fun GHC.Err.undefined () Int) "
CRASH: -1
which is still worth fixing.
The code below crashes with
Unknown func-sort
error.The problem is that PLE generates a
llen Nil
term hitting the bugs expected in https://github.com/ucsd-progsys/liquid-fixpoint/blob/develop/src/Language/Fixpoint/Types/Theories.hs#L121-L125A workaround is to introduce a
List Int -> Int
function (e.g., by uncommenting theworkaround
function). A proper fix should addList Int -> Int
in the sorts of sortEnv (here: https://github.com/ucsd-progsys/liquid-fixpoint/blob/develop/src/Language/Fixpoint/Solver/Sanitize.hs#L402) This is done for reflected functions but not for measures. (Does fixpoint have access to the measure definitions?)This should be a new bug, since measures used to be real SMT functions and did not require the
apply
defunctionalization.