You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
For my use case, I need a proof tree in all cases whenever the query is UNSAT. I wanted to remove cases where UNSAT was obtained in the preprocessing step itself. For this, I made the following changes:
1.set PREPROCESS_INPUT_QUERY to false in GlobalConfiguration.cpp
2.set PREPROCESSOR_ELIMINATE_VARIABLES to false in GlobalConfiguration.cpp
When I try to run it for a particular network, I get the following error:
"Caught a MarabouError. Code: 8. Message: Error! Have 288 infinite bounds"
From my understanding, the bounds on the input nodes haven't been propagated further. How can I correctly turn off the preprocesing step?
The text was updated successfully, but these errors were encountered:
For my use case, I need a proof tree in all cases whenever the query is UNSAT. I wanted to remove cases where UNSAT was obtained in the preprocessing step itself. For this, I made the following changes:
1.set PREPROCESS_INPUT_QUERY to false in GlobalConfiguration.cpp
2.set PREPROCESSOR_ELIMINATE_VARIABLES to false in GlobalConfiguration.cpp
When I try to run it for a particular network, I get the following error:
"Caught a MarabouError. Code: 8. Message: Error! Have 288 infinite bounds"
From my understanding, the bounds on the input nodes haven't been propagated further. How can I correctly turn off the preprocesing step?
The text was updated successfully, but these errors were encountered: