Merge pull request #2468 from ucsd-progsys/issue-728

Test issue728 branch of fixpoint
ucsd-progsys · Dec 23, 2024 · 80be93f · 80be93f
2 parents 791567f + 9307f32
commit 80be93f
Show file tree

Hide file tree

Showing 4 changed files with 37 additions and 2 deletions.
diff --git a/liquid-fixpoint b/liquid-fixpoint
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/WiredIn.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/WiredIn.hs
@@ -41,6 +41,7 @@ import Language.Haskell.Liquid.Types.Variance
 import Language.Haskell.Liquid.Types.PredType
 
 -- import Language.Fixpoint.Types hiding (panic)
+import qualified Language.Fixpoint.Types.Config as F
 import qualified Language.Fixpoint.Smt.Theories as F
 import qualified Language.Fixpoint.Types as F
 import           Data.Bifunctor (first)
@@ -93,7 +94,7 @@ wiredTheorySortedSyms =
     | s <- wiredTheorySyms
     , let srt = F.tsSort $
                   fromMaybe (panic Nothing ("unknown symbol: " ++ show s)) $
-                    F.lookupSEnv s (F.theorySymbols [])
+                    F.lookupSEnv s (F.theorySymbols F.Z3 [])
     ]
   where
     wiredTheorySyms =

diff --git a/stack.yaml b/stack.yaml
@@ -26,6 +26,19 @@ extra-deps:
 - store-core-0.4.4.6
 - git: https://github.com/qnikst/ghc-timings-report
   commit: 45ef3498e35897712bde8e002ce18df6d55f8b15
+- containers-0.7
+- ghc-9.10.1
+- ghc-internal-9.1001.0
+- Cabal-syntax-3.10.3.0@sha256:c2ca36499bf9365726968b1e11a757e6d846c47cdf0c2c26a003698fd3c300fe,7431
+- binary-0.8.9.2@sha256:03381e511429c44d13990c6d76281c4fc2468371cede4fe684b0c98d9b7d5f5a,6611
+- containers-0.6.8@sha256:bb2bec1bbc6b39a7c97cd95e056a5698ec45beb5d8feb6caae12af64e4bd823c,2670
+- ghc-boot-9.10.1@sha256:90fc95026568d3e7315f5f1d9481714002449ae4daed44e481b3ba0e1b32f61e,3227
+- ghc-heap-9.10.1@sha256:15ab60f08d6f4adcf423729fac0b40ee6a7d7d19942c6a5d190319a1c71b7e7c,2044
+- hpc-0.7.0.2@sha256:1c3c300837615288e9fe2e691f26bc8b047550c4bd2dd8dace55a58049ee1ec3,1113
+- parsec-3.1.17.0@sha256:8407cbd428d7f640a0fff8891bd2f7aca13cebe70a5e654856f8abec9a648b56,5149
+- template-haskell-2.22.0.0@sha256:463e87c76794859c861c95517329483282af8b079c02084755cc4bd1ae41d5ae,2151
+- text-2.1.1@sha256:78c3fb91055d0607a80453327f087b9dc82168d41d0dca3ff410d21033b5e87d,10653
+
 
 allow-newer: true
 allow-newer-deps:

diff --git a/stack.yaml.lock b/stack.yaml.lock
@@ -50,6 +50,27 @@ packages:
   original:
     commit: 45ef3498e35897712bde8e002ce18df6d55f8b15
     git: https://github.com/qnikst/ghc-timings-report
+- completed:
+    hackage: containers-0.7@sha256:e9b5fdcc609159410d408c47e0be13663bb0b4a42a5183b52aa0ac9c99e1dfec,2668
+    pantry-tree:
+      sha256: 265b0a6110df990b5f9f04d21856333ed5ed66f37a4b0a0215901d831f69629b
+      size: 2954
+  original:
+    hackage: containers-0.7
+- completed:
+    hackage: ghc-9.10.1@sha256:a281e1b3e7fb3fee7ba8c4b1a5b25da572b6ceb771a0037824df583fd46486f0,27483
+    pantry-tree:
+      sha256: 248912ad66a07c03086314cd977686d3adc1b1d05592e36c45e7383c090a5f5e
+      size: 53915
+  original:
+    hackage: ghc-9.10.1
+- completed:
+    hackage: ghc-internal-9.1001.0@sha256:dfa39788bc81ede2db08080a93ac8819e57a8d6df955243dcb4af550982fa5e7,15281
+    pantry-tree:
+      sha256: fa3749886ee8f60d07feb9a3009513af0273aedf38519d8121002b32e6639122
+      size: 22661
+  original:
+    hackage: ghc-internal-9.1001.0
 snapshots:
 - completed:
     sha256: fa3b5bc91ba72486026c6d9644df505eba3af4180ce072dd026064c62de92876
+10 −2		.circleci/config.yml
+10 −0		.github/workflows/cabal.yml
+14 −4		.github/workflows/stack.yml
+0 −8		TODO.md
+10 −10		src/Language/Fixpoint/Horn/Transformations.hs
+4 −0		src/Language/Fixpoint/Smt/Interface.hs
+6 −7		src/Language/Fixpoint/Smt/Serialize.hs
+74 −47		src/Language/Fixpoint/Smt/Theories.hs
+0 −19		src/Language/Fixpoint/Solver/Monad.hs
+4 −4		src/Language/Fixpoint/Solver/PLE.hs
+9 −9		src/Language/Fixpoint/Solver/Sanitize.hs
+2 −1		src/Language/Fixpoint/Types/Config.hs
+2 −2		src/Language/Fixpoint/Types/Names.hs
+16 −16		tests/horn/pos/scrape01.smt2
+5 −0		tests/test.hs