Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Segfault sygus-stream true, sygus-verify-subcall false, sygus-inference true #141

Closed
wintered opened this issue Mar 21, 2020 · 1 comment

Comments

@wintered
Copy link

Hi,
For this formula:

% cvc4-d80192c --quiet bug.smt2
CVC4 suffered a segfault.
Offending address is 0x0
Looks like a NULL pointer was dereferenced.
Aborted
% cat bug.smt2
(set-option :sygus-stream true) 
(set-option :sygus-verify-subcall false)   
(set-option :sygus-inference true)   
(declare-fun x () Real)   
(assert (<= 0 0.84)) 
(assert (> (sin 238) 0.85)) 
(assert (> (- 52 x 0) 0)) 
(assert (> (/ 236 0 x) 0)) 
(check-sat)  

CVC4 throws out a segmentation fault.

OS: Ubuntu 18.04
Commit: d80192c

@ajreynol ajreynol transferred this issue from cvc5/cvc5 Mar 21, 2020
@ajreynol
Copy link
Member

ajreynol commented Nov 3, 2021

sygus-verify-subcall no longer exists.

@ajreynol ajreynol closed this as completed Nov 3, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants