diff --git a/src/Language/Hasmtlib/Example/Transcendental.hs b/src/Language/Hasmtlib/Example/Transcendental.hs index 281458b..5e196bd 100644 --- a/src/Language/Hasmtlib/Example/Transcendental.hs +++ b/src/Language/Hasmtlib/Example/Transcendental.hs @@ -4,15 +4,14 @@ import Language.Hasmtlib main :: IO () main = do - res <- solveWith @SMT (solver cvc5) $ do + res <- solveWith @SMT (solver $ debugging verbosely cvc5) $ do setLogic "ALL" x <- var @RealSort - assert $ x >? sin 3 + assert $ 0 === sin x + assert $ x >? 0 return x print res - - return ()