sarsko / CreuSAT

CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.
MIT License
609 stars 11 forks source link

Thesis Typo: Lit Struct in Section 3.3 #43

Open mathatter997 opened 3 months ago

mathatter997 commented 3 months ago

Excellent project and thesis! Although I'm not finished reading it :)

I think there's a minor typo for Lit struct in section 3.3. You define Lit as having a polarity bool. But this is subsequently changed to value in later snippets. Changing it value should fix things.

Screenshot 2024-07-15 at 2 59 33 PM
sarsko commented 3 months ago

Thanks!

You are indeed correct, it says polarity when introducing Lit, and then subsequently value is used.

Seems like Overleaf has shittified their free-tier to the point that the thesis no longer builds. I'll fix my local LaTeX install over the weekend and fix it.