[Python] Shall we really invoke the SMT solver for this simple Python program?

[lucasccordeiro]

I would expect our constant propagation algorithm to solve this case easily without calling the SMT solver.

class MyClass:
    def __init__(self, value: int):
        self.data:int = value


obj1 = MyClass(5)
assert(obj1.data == 5)
obj1.data = 10
assert(obj1.data == 10)
obj1.data = 20
assert(obj1.data == 20)

obj2 = MyClass(30)
assert(obj2.data == 30)
obj2.data = 40
assert(obj2.data == 40)

$ esbmc main.py
ESBMC version 7.4.0 64-bit x86_64 linux
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
Parsing main.py
Converting
Generating GOTO Program
GOTO program creation time: 0.039s
GOTO program processing time: 0.000s
Starting Bounded Model Checking
Symex completed in: 0.000s (14 assignments)
Slicing time: 0.000s (removed 4 assignments)
Generated 9 VCC(s), 5 remaining after simplification (10 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.000s
BMC program time: 0.001s

VERIFICATION SUCCESSFUL

[lucasccordeiro]

It looks like we don't propagate the store operations involving constants:

Program constraints:
// 0 file main.py line 3 column 8 function MyClass
/* 1 */ obj1&0#1 == (obj1&0#0 WITH [data:=5])

// 3  (assertion)
/* 2 */ (assert)execution_statet::\guard_exec?0!0 => obj1&0#1.data == 5

// 4 file main.py line 8 column 0
/* 3 */ obj1&0#2 == (obj1&0#1 WITH [data:=10])

// 5  (assertion)
/* 4 */ (assert)execution_statet::\guard_exec?0!0 => obj1&0#2.data == 10

// 6 file main.py line 10 column 0
/* 5 */ obj1&0#3 == (obj1&0#2 WITH [data:=20])

// 7  (assertion)
/* 6 */ (assert)execution_statet::\guard_exec?0!0 => obj1&0#3.data == 20

// 0 file main.py line 3 column 8 function MyClass
/* 7 */ obj2&0#1 == (obj2&0#0 WITH [data:=30])

// 9  (assertion)
/* 8 */ (assert)execution_statet::\guard_exec?0!0 => obj2&0#1.data == 30

// 10 file main.py line 15 column 0
/* 9 */ obj2&0#2 == (obj2&0#1 WITH [data:=40])

// 11  (assertion)
/* 10 */ (assert)execution_statet::\guard_exec?0!0 => obj2&0#2.data == 40

[fbrausse]

Might it be because WITH is not propagated? See #1398.