Commits · master · Vincent Laporte / iprover

Browse files

Sep 29, 2023
- minor · 8bf2d733
  Konstantin Korovin authored Sep 29, 2023
  
  8bf2d733
Aug 05, 2023
- Merge branch 'add-ci' into 'master' · 368c334c
  Konstantin Korovin authored Aug 05, 2023
  368c334c
Aug 04, 2023
- add comments and use a pre-build static z3 · 7f120187
  Boris Shminke authored Aug 04, 2023
  
  7f120187
Aug 01, 2023
- add CI · af5a59dc
  Boris Shminke authored Apr 25, 2023 and Boris Shminke committed Aug 01, 2023
  
  af5a59dc
Jul 13, 2023
- Merge branch '2023_07_dbg' · 11831c13
  Konstantin Korovin authored Jul 13, 2023
  
  11831c13
- TESTS · efadb7dd
  Konstantin Korovin authored Jul 13, 2023
  
  efadb7dd
- run_tests.sh · b854c8dc
  Konstantin Korovin authored Jul 13, 2023
  
  b854c8dc
- minor clean-up · 1cbca526
  Konstantin Korovin authored Jul 13, 2023
  
  1cbca526
- version 3.8.1 · a22f09bb
  Konstantin Korovin authored Jul 13, 2023
  
  a22f09bb
Jul 12, 2023
- util/libz3.a; static linking with z3 in git · 8c70138a
  Konstantin Korovin authored Jul 12, 2023
  
  8c70138a
Jul 11, 2023
- .merlin · a0bf2b37
  Konstantin Korovin authored Jul 11, 2023
  
  a0bf2b37
Jul 09, 2023
- fix: smt_shared_clauses · 6ae6e418
  Konstantin Korovin authored Jul 09, 2023
  
  6ae6e418
Jul 08, 2023
- fix · 82c99876
  Konstantin Korovin authored Jul 08, 2023
  
  82c99876
- fix: adding outside clauses to the smt solver · 1dbb1f84
  Konstantin Korovin authored Jul 08, 2023
  
  1dbb1f84
- --prep_eq_flat_all_gr: conj/non-conj processed jointly · 231fafd1
  Konstantin Korovin authored Jul 08, 2023
  
  231fafd1
Jul 07, 2023
- --prep_eq_flat_all_gr · 18fb7bd9
  Konstantin Korovin authored Jul 07, 2023
  
  18fb7bd9
- eq_flattening: assign neg_conj to new gen clauses and symb · eb0512c4
  Konstantin Korovin authored Jul 07, 2023
  
  eb0512c4
Jul 06, 2023
- eq_flattening: add negated_conjecture to the final clause (but not def equations) · b8af1f4d
  Konstantin Korovin authored Jul 07, 2023
  
  b8af1f4d
- src/eq_flattening.ml · 122cd646
  Konstantin Korovin authored Jul 06, 2023
  
  122cd646
- --prep_eq_flat_conj · b6ecd41c
  Konstantin Korovin authored Jul 06, 2023
  
  b6ecd41c
Jul 05, 2023
- symbolDB new split symb -> new def symb · 36308f00
  Konstantin Korovin authored Jul 06, 2023
  
  36308f00
- Symbol.Split -> Symbol.Definition · 3d59dadb
  Konstantin Korovin authored Jul 05, 2023
  
  3d59dadb
- symbolDB:split symbols not clashing with input · c3883d1c
  Konstantin Korovin authored Jul 05, 2023
  
  c3883d1c
Jun 29, 2023
- fix: finite models with non-monot types: suppress unsat · 149955f0
  Konstantin Korovin authored Jun 29, 2023
  
  149955f0
Jun 28, 2023
- next · 72e448d0
  Konstantin Korovin authored Jun 28, 2023
  
  72e448d0
- is_rat_real as uninterpreted · 5719e70d
  Konstantin Korovin authored Jun 28, 2023
  
  5719e70d
- is_int_real · 40c5fbd8
  Konstantin Korovin authored Jun 28, 2023
  
  40c5fbd8
Jun 09, 2023
- fixed vclausify_rel · ce87a6fe
  Konstantin Korovin authored Jun 09, 2023
  
  ce87a6fe
May 31, 2023
- fix: suppressed sat when it is not needed · 86e67f3e
  Konstantin Korovin authored May 31, 2023
  
  86e67f3e
- fix: suppressed sat when it is not needed · fb37bb1a
  Konstantin Korovin authored May 31, 2023
  
  fb37bb1a
- TESTS/list2_uf_sat.smt2 · d6a27c3e
  Konstantin Korovin authored May 31, 2023
  
  d6a27c3e
May 27, 2023
- fix: fof ext parsing · e998d44f
  Konstantin Korovin authored May 27, 2023
  
  e998d44f
May 23, 2023
- Merge branch '2023_smt_share' of gitlab.com:korovin/iprover into 2023_smt_share · 2f8fc577
  Konstantin Korovin authored May 23, 2023
  
  2f8fc577
- util/vclausify_rel_mac ANIA · c8bb610b
  Konstantin Korovin authored May 23, 2023
  
  c8bb610b
- vclausify_rel: ANIA · fcc1fd57
  Konstantin Korovin authored May 23, 2023
  
  fcc1fd57
- fix · 222d50b8
  Konstantin Korovin authored May 23, 2023
  
  222d50b8
- fix · b5665953
  Konstantin Korovin authored May 23, 2023
  
  b5665953
- fix · 7a90d191
  Konstantin Korovin authored May 23, 2023
  
  7a90d191
May 22, 2023
- comments · eae6199e
  Konstantin Korovin authored May 22, 2023
  
  eae6199e
- added: --ints_to_smt_sover/--res_to_smt_sover · 3a885c44
  Konstantin Korovin authored May 22, 2023
  
  3a885c44