all tests pass; try flux

ucsd-progsys · Dec 18, 2024 · 68581b2 · 68581b2
1 parent 6cafaac
commit 68581b2
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 6 deletions.
diff --git a/.circleci/config.yml b/.circleci/config.yml
@@ -19,7 +19,14 @@ jobs:
             sudo cp z3-4.8.7-x64-ubuntu-16.04/include/* /usr/local/include
             rm -rf z3-4.8.7-x64-ubuntu-16.04
             z3 --version
-
+      - run:
+          name: Install cvc5
+          command: |
+            wget https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.0/cvc5-Linux-x86_64-static.zip
+            unzip cvc5-Linux-x86_64-static.zip
+            rm -f cvc5-Linux-x86_64-static.zip
+            sudo cp z3-4.8.7-x64-ubuntu-16.04/bin/z3 /usr/local/bin
+            
       - checkout
       - restore_cache:
           keys:

diff --git a/src/Language/Fixpoint/Smt/Serialize.hs b/src/Language/Fixpoint/Smt/Serialize.hs
@@ -56,18 +56,19 @@ smt2dataname env (DDecl tc as _) = parenSeqs [name, n]
 smt2datactors :: SymEnv -> DataDecl -> Builder
 smt2datactors env (DDecl _ as cs)
   | as > 0       = parenSeqs ["par", parens tvars, parens ds]
-  | otherwise    = parenSeqs [                     parens ds]
+  | otherwise    =                                 parens ds
   where
     tvars        = smt2many (smt2TV <$> [0..(as-1)])
     smt2TV       = smt2 env . SVar
     ds           = smt2many (smt2ctor env as <$> cs)
 
 smt2ctor :: SymEnv -> Int -> DataCtor -> Builder
-smt2ctor env _  (DCtor c [])  = smt2 env c
-smt2ctor env as (DCtor c fs)  = parenSeqs [smt2 env c, fields]
 
-  where
-    fields                 = smt2many (smt2field env as <$> fs)
+smt2ctor env as (DCtor c fs)  = parenSeqs (smt2 env c : (smt2field env as <$> fs))
+-- smt2ctor env _  (DCtor c [])  = parens (smt2 env c)
+-- smt2ctor env as (DCtor c fs)  = parenSeqs [smt2 env c, fields]
+  -- where
+  --   fields                 = smt2many (smt2field env as <$> fs)
 
 smt2field :: SymEnv -> Int -> DataField -> Builder
 smt2field env as d@(DField x t) = parenSeqs [smt2 env x, smt2SortPoly d env $ mkPoly as t]