## Bug #7795

### Type constraints option for LA theories

0%

**Description**

Following Grigory answer, this code is a test for the assertion ordering than for the type constraints: assuming a >= 0 and b >= 0 we can easily derive that c >= 0.

The original code, suppose to run with type_constraints 1 and results in UNSAT. We can run the loop till 10 (no need for so many iterations). To prove claim 1 and 2 we need type-constraints 1, and using claim 1+2 we can prove claim 3 (I think via claims-opt option).

Older version of type-constraints use to work well. I think not all the added type-constraints are in the end added to the SMT query (can be the remove of incrementality).

=========================

The code:

int sum () { int s=0; unsigned n; for (int i = 0; i <10; i++) { n = nondetUInt(); s=s+n; } return s; } int main() { int a,b,c; a=sum(); assert(a>=0); b=sum(); assert(b>=0); c=a+b; assert(c>=0); }

Please add this test in the end to the regression test with reference to TACAS17 paper.

### History

#### #1 Updated by Karine Even Mendoza almost 3 years ago

type-constraints 0: does nothing

type-constraints 1: adds bounds to non-det declaration, that is

char a;

char b = a + 1;

(and (=< 128 a#0) (< a#0 128))

type-constraints 2: adds bounds to non-det declaration and add assert to other vars (to check overflow), that is

char a;

char b = a + 1;

assert (a < b);

> (and (and (=< 128 a#0) (< a#0 128)) // assume

(not (and

(< a b) // original assert

(and (=< 128 b#0) (< b#0 128)) // additional assert from type_constraints 2

))

// KE: I hope I am not wrong with this encoding, but the idea is that we add the constraints to the assert encoding and check its not (as if it were part of the assert :

assert(a < b && b.is_in_bounds);)

We can also run older version to see how it use to work.

#### #2 Updated by Martin Blicha almost 3 years ago

The example is missing function declaration.

unsigned int nondetUInt();

With that, the assertions are verified with type-constraints 1 and overflow is detected with type-constraints 2, as expected.