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

Unexpected UNSAT status during parameters resolving #1070

Open
CaelmBleidd opened this issue Oct 4, 2022 · 0 comments
Open

Unexpected UNSAT status during parameters resolving #1070

CaelmBleidd opened this issue Oct 4, 2022 · 0 comments
Assignees
Labels
comp-symbolic-engine Issue is related to the symbolic execution engine ctg-bug Issue is a bug

Comments

@CaelmBleidd
Copy link
Member

Description

Because of some reason we got an UNSAT status for a state during parameters resolving in an invocation processing. It happens inside org.utbot.engine.Traverser#initStringLiteral method, but it is not clear, how it is possible to get unsat because of creating a new object.

To Reproduce

Steps to reproduce the behavior:

  1. Run the 'UTBotTest' project in debug IntelliJ Idea
  2. Set a breakpoint inside of the code that drops unsat states in commonInvokePart
  3. Use plugin to generate tests for class MapOperate

Expected behavior

The breakpoint should never be reached.

Actual behavior

UTBot reaches the breakpoint.

Environment

There is no specific environment, but it might take a long time to reach it.

Additional context

There is no additional context.

@CaelmBleidd CaelmBleidd added ctg-bug Issue is a bug comp-symbolic-engine Issue is related to the symbolic execution engine labels Oct 4, 2022
@CaelmBleidd CaelmBleidd self-assigned this Oct 4, 2022
@CaelmBleidd CaelmBleidd moved this to Todo in UTBot Java Oct 4, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
comp-symbolic-engine Issue is related to the symbolic execution engine ctg-bug Issue is a bug
Projects
Status: Todo
Development

No branches or pull requests

1 participant