Anzhela Sukhanova issues

Repositories
Issues
Comments

Results 2 issues of


                                            Anzhela Sukhanova

Quantifier elimination for the theory of bit vectors

PR implements the quantifier elimination for BV formulas of a certain structure according to the [paper](https://www.researchgate.net/publication/228686393_On_the_expansion_N_2x_of_Presburger_arithmetic). Supported structure: a conjunction of inequalities/equalities between a bound variable in a linear term...

Incorrect model

Hello! For ``` (set-logic HORN) (declare-fun |state| ( Bool Bool Bool Bool Int Int Int ) Bool) (assert (forall ((C Int) (D Int) (E Int)) (state false true false false...