Skip to content

Instantly share code, notes, and snippets.

@livnev

livnev/Vat_tune_succ.out

Created August 26, 2018 22:16
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save livnev/86a689641944c563b1cf26e4fe33c86b to your computer and use it in GitHub Desktop.
Save livnev/86a689641944c563b1cf26e4fe33c86b to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Vat_tune_succ.out
behaviour
HEAD DELTAC
├ 0 ¬( 0 < ABI_dink )
│ ├ 0 ¬( ABI_dink < 0 )
│ │ ├ 0 ¬( 0 < ABI_dart )
│ │ │ ├ 0 ✓ ¬( ABI_dart < 0 )
│ │ │ └ 1 ABI_dart < 0
│ │ │ ├ 0 ✓ ¬( Rate * ABI_dart < 0 )
│ │ │ └ 1 ✓ Rate * ABI_dart < 0
│ │ └ 1 0 < ABI_dart
│ │ ├ 0 ✓ ¬( 0 < Rate * ABI_dart )
│ │ └ 1 ✓ 0 < Rate * ABI_dart
│ └ 1 ABI_dink < 0
│ ├ 0 ¬( 0 < ABI_dart )
│ │ ├ 0 ✓ ¬( ABI_dart < 0 )
│ │ └ 1 ABI_dart < 0
│ │ ├ 0 ✓ ¬( Rate * ABI_dart < 0 )
│ │ └ 1 ✓ Rate * ABI_dart < 0
│ └ 1 0 < ABI_dart
│ ├ 0 ✓ ¬( 0 < Rate * ABI_dart )
│ └ 1 ✓ 0 < Rate * ABI_dart
└ 1 0 < ABI_dink
├ 0 ¬( 0 < ABI_dart )
│ ├ 0 ✓ ¬( ABI_dart < 0 )
│ └ 1 ABI_dart < 0
│ ├ 0 ✓ ¬( Rate * ABI_dart < 0 )
│ └ 1 ✓ Rate * ABI_dart < 0
└ 1 0 < ABI_dart
├ 0 ✓ ¬( 0 < Rate * ABI_dart )
└ 1 ✓ 0 < Rate * ABI_dart
Symbolic expression for gas remaining at the end of execution, where `Gas` is initial gas:
#if notBool Ink_u + ABI_dink == 0 andBool Ink_u == 0 #then #if notBool Art_u + ABI_dart == 0 andBool Art_u == 0 #then #if notBool Art_i + ABI_dart == 0 andBool Art_i == 0 #then #if notBool Dai +
Rate * ABI_dart == 0 andBool Dai == 0 #then #if notBool Debt + Rate * ABI_dart == 0 andBool Debt == 0 #then Gas - 109580 #else Gas - 94580 #fi #else #if notBool Debt + Rate * ABI_dart == 0 andBool Debt == 0
#then Gas - 94580 #else Gas - 79580 #fi #fi #else #if notBool Dai + Rate * ABI_dart == 0 andBool Dai == 0 #then #if notBool Debt + Rate * ABI_dart == 0 andBool Debt == 0 #then Gas - 94580 #else Gas - 79580 #fi
#else #if notBool Debt + Rate * ABI_dart == 0 andBool Debt == 0 #then Gas - 79580 #else Gas - 64580 #fi #fi #fi #else #if notBool Art_i + ABI_dart == 0 andBool Art_i == 0 #then #if notBool Dai + Rate * ABI_dart
== 0 andBool Dai == 0 #then #if notBool Debt + Rate * ABI_dart == 0 andBool Debt == 0 #then Gas - 94580 #else Gas - 79580 #fi #else #if notBool Debt + Rate * ABI_dart == 0 andBool Debt == 0 #then Gas - 79580
#else Gas - 64580 #fi #fi #else #if notBool Dai + Rate * ABI_dart == 0 andBool Dai == 0 #then #if notBool Debt + Rate * ABI_dart == 0 andBool Debt == 0 #then Gas - 79580 #else Gas - 64580 #fi #else #if notBool
Debt + Rate * ABI_dart == 0 andBool Debt == 0 #then Gas - 64580 #else Gas - 49580 #fi #fi #fi #fi #else #if notBool Art_u + ABI_dart == 0 andBool Art_u == 0 #then #if notBool Art_i + ABI_dart == 0 andBool Art_i
== 0 #then #if notBool Dai + Rate * ABI_dart == 0 andBool Dai == 0 #then #if notBool Debt + Rate * ABI_dart == 0 andBool Debt == 0 #then Gas - 94580 #else Gas - 79580 #fi #else #if notBool Debt + Rate * ABI_dart
== 0 andBool Debt == 0 #then Gas - 79580 #else Gas - 64580 #fi #fi #else #if notBool Dai + Rate * ABI_dart == 0 andBool Dai == 0 #then #if notBool Debt + Rate * ABI_dart == 0 andBool Debt == 0 #then Gas - 79580
#else Gas - 64580 #fi #else #if notBool Debt + Rate * ABI_dart == 0 andBool Debt == 0 #then Gas - 64580 #else Gas - 49580 #fi #fi #fi #else #if notBool Art_i + ABI_dart == 0 andBool Art_i == 0 #then #if notBool
Dai + Rate * ABI_dart == 0 andBool Dai == 0 #then #if notBool Debt + Rate * ABI_dart == 0 andBool Debt == 0 #then Gas - 79580 #else Gas - 64580 #fi #else #if notBool Debt + Rate * ABI_dart == 0 andBool Debt == 0
#then Gas - 64580 #else Gas - 49580 #fi #fi #else #if notBool Dai + Rate * ABI_dart == 0 andBool Dai == 0 #then #if notBool Debt + Rate * ABI_dart == 0 andBool Debt == 0 #then Gas - 64580 #else Gas - 49580 #fi
#else #if notBool Debt + Rate * ABI_dart == 0 andBool Debt == 0 #then Gas - 49580 #else Gas - 34580 #fi #fi #fi #fi #fi
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment