Commits on Jul 24, 2023

1. Propagate equalities within int2bv …

   This patch adds some reasoning support in bitv_rel for equalities and
   disequalities between `int2bv` terms. More specifically, when an
   equality or disequality (~ stands for either `=` or `distinct`):
   
     `(~ ((_ int2bv n) t) ((_ int2bv n) u))`
   
   is asserted, we also assert that `t` and `u` are congruent (resp.
   noncongruence) modulo `2^n`, i.e.
   
     `(~ (mod (- t u) (pow 2 n)) 0)`
   
   This allows recovering some reasoning power involving bitvector terms
   containing `int2bv`, and in particular terms involving bitvector
   arithmetic (since bitvector arithmetic is currently implemented using
   `int2bv`).

   

   bclement-ocp committed Jul 24, 2023
   Configuration menu

   • View commit details
   • Copy full SHA for 10e8444
   • Browse repository at this point

   Copy the full SHA

   10e8444 View commit details

   Browse the repository at this point in the history