flux seems to work

ucsd-progsys · Dec 18, 2024 · be3e09b · be3e09b
1 parent a0eea6c
commit be3e09b
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 11 deletions.
diff --git a/TODO.md b/TODO.md
@@ -1,8 +1 @@
 # TODO
-
-## CVC5
-
-- [x] bitv.smt2
-- [x] str00.smt2
-- [x] scrape01.smt2
-- [] horn-pos-cvc5.ple_list01_adt.smt2
diff --git a/src/Language/Fixpoint/Smt/Serialize.hs b/src/Language/Fixpoint/Smt/Serialize.hs
@@ -65,10 +65,6 @@ smt2datactors env (DDecl _ as cs)
 smt2ctor :: SymEnv -> Int -> DataCtor -> Builder
 
 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]