HW7 = in QF_LIA - Githubissues

swtv-kaist / cs458-fall22

1 stars 0 forks source link

HW7 = in QF_LIA #30

Open Akkanit opened 1 year ago

Akkanit commented 1 year ago

I wonder about = so in QF_LIA in the formula, I can use = for both

Assignment: a = b+1
Comparison: If(a == b+1) right?

moonzoo commented 1 year ago

"=" in SMTlib specification means equivalence, not assignment (in logic specification, there is no assignment). That is why you should use SSA form to model assignment by renaming variables.