More debug printing, enabling tests

src/EVM/SymExec.hs

@@ -627,8 +627,10 @@ verify solvers opts preState maybepost = do
         -- Dispatch the remaining branches to the solver to check for violations
         results <- flip mapConcurrently withQueries $ \(query, leaf) -> do
           res <- checkSat solvers query
+          when conf.debug $ putStrLn $ "   SMT result: " <> show res
           pure (res, leaf)
         let cexs = filter (\(res, _) -> not . isUnsat $ res) results
+        when conf.debug $ putStrLn $ "   Found " <> show (length cexs) <> " potential counterexample(s) in call " <> call
         pure $ if Prelude.null cexs then (expr, [Qed ()]) else (expr, fmap toVRes cexs)
   where
     getCallPrefix :: Expr Buf -> String

test/test.hs

@@ -1768,7 +1768,7 @@ tests = testGroup "hevm"
           check coinbase (SymAddr "coinbase")
           check a (SymAddr "freshSymAddr1")
           check arg (SymAddr "arg1")
-    , ignoreTest $ test "vm.load fails for a potentially aliased address" $ do
+    , test "vm.load fails for a potentially aliased address" $ do
         Just c <- solcRuntime "C"
           [i|
             interface Vm {
@@ -1784,7 +1784,7 @@ tests = testGroup "hevm"
         (_, [Cex _]) <- withDefaultSolver $ \s ->
           verifyContract s c Nothing [] defaultVeriOpts Nothing (Just $ checkBadCheatCode "load(address,bytes32)")
         pure ()
-    , ignoreTest $ test "vm.store fails for a potentially aliased address" $ do
+    , test "vm.store fails for a potentially aliased address" $ do
         Just c <- solcRuntime "C"
           [i|
             interface Vm {