Fixes (#56)

* Update AllDirect.spec

* Update config.yml

* Update config.yml

* Update structs.spec

* Update config.yml

Author: liav-certora

CVLByExample/Structs/BankAccounts/certora/specs/structs.spec

@@ -104,12 +104,12 @@ rule integrityOfCustomerKeyRule(address a, method f) {
 
 /// Represent the sum of all accounts of all users
 /// sum _customers[a].accounts[i].accountBalance 
-ghost mathint sumBalances {
+persistent ghost mathint sumBalances {
     init_state axiom sumBalances == 0;
 }
 
 /// Mirror on a struct _customers[a].accounts[i].accountBalance
-ghost mapping(address => mapping(uint256 => uint256)) accountBalanceMirror {
+persistent ghost mapping(address => mapping(uint256 => uint256)) accountBalanceMirror {
     init_state axiom forall address a. forall uint256 i. accountBalanceMirror[a][i] == 0;
 }
 

CVLByExample/Summarization/Library/DirectSummary/certora/specs/AllDirect.spec

@@ -2,8 +2,6 @@
  * For each function called from Test.sol a summary is provided.
  */
 
-using TestLibrary as testlibrary;
-
 methods {
     // functions declared in TestLibrary
     function TestLibrary.calleeInternal() internal returns bool => ALWAYS(true);
@@ -35,7 +33,3 @@ rule callOverloadedInInterfaceExternal(env e) {
 rule callIOverloadedInInterfaceExternal(env e) { 
     assert (callIOverloadedInInterfaceExternal(e), "Unresolved function not summarized as expected") ;        
 }
-
-rule callSummarizedFromCVL(env e) {
-    assert (testlibrary.calleeExternal(e), "Function called from CVL is not summarized");
-}