Skip to content

[QUESTION] How to be sure to retrieve the correct boolean for a variable (ex.: int) ? #6948

Closed
@PeterMacGonagan

Description

@PeterMacGonagan

Hello,

I use CBMC to generate CNF from little math problems (--dimacs).
I use external solver to find the solutions. CBMC is able to compute the correct solution (with minisat). I use --trace-compact to see the solutions.

I would like to get the equivalent boolean of my variables. --compact-trace is able to do it.

I can observe that at the end of dimacs file there are some lines of this kind:

c main::1::b2!0@1#2 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197

which derives from:
int b2;

We can observe 32 booleans (=4 bytes).

c main::1::b2!0@1#2
166 167 168 169 170 171 172 173
174 175 176 177 178 179 180 181
182 183 184 185 186 187 188 189
190 191 192 193 194 195 196 197

Could you confirm me that there are expressed from LSB (166) to MSB (197) (Left to Right)?
Could you tell me how to be sure to retrieve the correct boolean for my variables? Note: I just have 16 integers to retrieve. I'll write a little parser.

In fact, I'm a little confused about the fact that b2 has two "equivalences":

[line 10010] c main::1::b2!0@1#2 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197

[line 10186] c main::1::b2!0@1#1 3058 3059 3060 3061 3062 3063 3064 3065 3066 3067 3068 3069 3070 3071 3072 3073 3074 3075 3076 3077 3078 3079 3080 3081 3082 3083 3084 3085 3086 3087 3088 3089

Does it means that: 166=3058, 167=3059, etc. ?

What' is the meaning of: c main::1::b2!0@1#2
It's was in c langage
function main
Thread 1???
Variable b2
!0@1#2 or !0@1#1

Thank you in advance.

Metadata

Metadata

Labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions