diff --git a/TODO.md b/TODO.md
index 54c0a0f3a..464090415 100644
--- 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
index be2a0e21d..d14a2ead9 100644
--- 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]