cvc5 / LFSC

LFSC Proof Checker
Other
11 stars 9 forks source link

Seg fault on a simple example #59

Closed BrunoDutertre closed 2 years ago

BrunoDutertre commented 2 years ago

Here's a one-line example from rlfsc:

(declare T (! sc (^ (mp_ifneg 10 0 1) 1) type))

On this example, lfscc seg faults.

A debugger shows that the problem is at line 476 of check.cpp:

   Expr* trm = check(true, progret);

In this call it's possible for progret to be NULL (and computed is NULL by default), but check requires one of them to be non-null.

ajreynol commented 2 years ago

Thanks for pointing this out, I'm working on a fix for this and #60 which is related.