Commits · 795220a87dc1878389bb4385b644bc6cc2386d27 · Marek Chalupa / slowbeast

May 03, 2021
- bself: on the first hit, unwind only twice · 795220a8
  Marek Chalupa authored May 03, 2021
  
  795220a8
- relations: use incremental solving · aee9109a
  Marek Chalupa authored May 03, 2021
  
  aee9109a
- Revert "union sets from exits" · a6da382a
  Marek Chalupa authored May 03, 2021
  a6da382a
- bself: store inductive sets once we have them · af5a7dab
  Marek Chalupa authored May 03, 2021
  af5a7dab
Apr 30, 2021
- union sets from exits · 4cb07686
  Marek Chalupa authored Apr 30, 2021
  
  4cb07686
- unwind loop only when hit for the first time · 7156b92a
  Marek Chalupa authored Apr 30, 2021
  
  7156b92a
- add scc condensation · 74a7d81b
  Marek Chalupa authored Apr 30, 2021
  
  74a7d81b
- bself: do not do lookahead in overapprox · b512582e
  Marek Chalupa authored Apr 30, 2021
  
  b512582e
Apr 29, 2021
- Revert "bse: remember the order of writes to memory" · 1ae1147a
  Marek Chalupa authored Apr 29, 2021
  1ae1147a
Apr 28, 2021
- tests: add a new test · 3a4826fd
  Marek Chalupa authored Apr 28, 2021
  
  3a4826fd
- bself: fix creating initial sets · 9f6325a6
  Marek Chalupa authored Apr 28, 2021
  
  9f6325a6
- BSELF: prune inductive sets · 6ab77610
  Marek Chalupa authored Apr 28, 2021
  6ab77610
- overapprox: fix a crash · ebff7b09
  Marek Chalupa authored Apr 28, 2021
  ebff7b09
- symexe mem: fix a check for uninit bytes · c2c60557
  Marek Chalupa authored Apr 28, 2021
  c2c60557
- bse: remember the order of writes to memory · 62d66147
  Marek Chalupa authored Apr 28, 2021
  62d66147
- solver: fix obtaining clauses · a994dd6f
  Marek Chalupa authored Apr 28, 2021
  
  a994dd6f
- solver: fix accessing non-symbolic value as symbolic · 19313569
  Marek Chalupa authored Apr 28, 2021
  
  19313569
- solver: remove implied clauses multiple times · a254a90f
  Marek Chalupa authored Apr 28, 2021
  
  a254a90f
- add a note · 1911f325
  Marek Chalupa authored Apr 28, 2021
  
  1911f325
- solver: do not solve reduced formulas · fb806c12
  Marek Chalupa authored Apr 28, 2021
  
  fb806c12
- solver: fix using inferred equalities · b9e5decd
  Marek Chalupa authored Apr 28, 2021
  b9e5decd
- solver: fix solving with reduced bitwith · 1e071937
  Marek Chalupa authored Apr 28, 2021
  1e071937
Apr 27, 2021
- enable solving with reduced bitwidth · 839f12d0
  Marek Chalupa authored Apr 27, 2021
  
  839f12d0
- fix rewriting polynomials · af49bfa1
  Marek Chalupa authored Apr 27, 2021
  af49bfa1
- Revert "symbolic: fix simplifying arith formula" · b4313396
  Marek Chalupa authored Apr 27, 2021
  b4313396
- solver: remove is_sat function · cfcc2057
  Marek Chalupa authored Apr 27, 2021
  
  cfcc2057
- solver: fix a concrete value · ea1f3555
  Marek Chalupa authored Apr 27, 2021
  
  ea1f3555
- symbolic: fix simplifying arith formula · 0d4254eb
  Marek Chalupa authored Apr 27, 2021
  0d4254eb
- arithformula: fix printing · f153ee28
  Marek Chalupa authored Apr 27, 2021
  
  f153ee28
- bse: remove invalid assertion · 7cd3600a
  Marek Chalupa authored Apr 27, 2021
  
  7cd3600a
- bse: fix running paths from the middle · 74b6d4e8
  Marek Chalupa authored Apr 27, 2021
  74b6d4e8
- bself: try using also constant cmp as assumptions · 72a097de
  Marek Chalupa authored Apr 27, 2021
  72a097de
- tests sumt4: increase timeout · 2b01c229
  Marek Chalupa authored Apr 27, 2021
  2b01c229
- bself: refactor overapprox SIS · 426bb11c
  Marek Chalupa authored Apr 27, 2021
  426bb11c
- bself: simplify generating relations · 920e9ebb
  Marek Chalupa authored Apr 27, 2021
  920e9ebb
- bself: refactor a bit · 5685f51d
  Marek Chalupa authored Apr 27, 2021
  5685f51d
- bself: do look-ahead step in extending · 0be8020c
  Marek Chalupa authored Apr 27, 2021
  0be8020c
- bself: refactor a bit · dc8d9b47
  Marek Chalupa authored Apr 27, 2021
  dc8d9b47
- bself: remove unused code · 3efc35cb
  Marek Chalupa authored Apr 27, 2021
  
  3efc35cb
- arithformula: support boolean constants · 0eddaa03
  Marek Chalupa authored Apr 27, 2021
  
  0eddaa03

Admin message