diff --git a/test/test.hs b/test/test.hs index 999587b48..4ab116aa5 100644 --- a/test/test.hs +++ b/test/test.hs @@ -3624,12 +3624,16 @@ checkEquiv a b = do if a == b then pure True else do when (opts.debug) $ liftIO $ putStrLn $ "Checking equivalence of " <> show a <> " and " <> show b x <- checkEquivBase (./=) a b True + when (opts.debug) $ liftIO $ putStrLn $ "UNSAT check, expect True: " <> show x y <- checkEquivBase (.==) a b False + when (opts.debug) $ liftIO $ putStrLn $ "SAT check, expect False: " <> show y pure $ (fromMaybe True x) && not (fromMaybe False y) checkEquivAndLHS :: (Typeable a, App m) => Expr a -> Expr a -> m Bool checkEquivAndLHS orig simp = do + opts <- readConfig let lhsConst = Expr.checkLHSConst simp + when (opts.debug) $ liftIO $ putStrLn $ "LHS const: " <> show lhsConst equiv <- checkEquiv orig simp pure $ lhsConst && equiv