NewCNF segfaults when a let is bound to another let.
(set-logic ALL)
(declare-fun p () Bool)
(declare-fun q () Bool)
(declare-fun r () Bool)
(assert (let ((b (let ((c (and r p))) c))) (or (=> q b) b)))
(check-sat)
$ vampire -newcnf on crash.smt2
% Aborted by signal SIGSEGV on crash.smt2
% Termination reason: Unknown
% Termination phase: NewCNF
Release build, commit 4844270.
Three things are load-bearing. The outer let has to be bound to another let: (let ((b (and r p))) (or (=> q b) b)) is answered normally. The inner body has to be a conjunction: (or r p) in its place does not trigger it. And the bound variable has to occur both under an implication and on its own.
Found while testing #894, and it reproduces with and without that branch, so it is independent of it.
NewCNF segfaults when a let is bound to another let.
Release build, commit 4844270.
Three things are load-bearing. The outer let has to be bound to another let:
(let ((b (and r p))) (or (=> q b) b))is answered normally. The inner body has to be a conjunction:(or r p)in its place does not trigger it. And the bound variable has to occur both under an implication and on its own.Found while testing #894, and it reproduces with and without that branch, so it is independent of it.