We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
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
(set-option :produce-models true)
For example, this formula
(set-logic QF_S) (set-option :produce-models true) (declare-const str1 String) (declare-const str2 String) (assert (= (str.++ str1 str2) "hello world")) (check-sat) (get-model)
leads to an exception, because it assumes that model generation is turned off, so the map that saves the model is empty.
The paramater theory_str_noodler_params::m_produce_models is probably set incorrectly in src/smt/params/theory_str_noodler_params.cpp.
theory_str_noodler_params::m_produce_models
src/smt/params/theory_str_noodler_params.cpp
The text was updated successfully, but these errors were encountered:
No branches or pull requests
For example, this formula
leads to an exception, because it assumes that model generation is turned off, so the map that saves the model is empty.
The paramater
theory_str_noodler_params::m_produce_models
is probably set incorrectly insrc/smt/params/theory_str_noodler_params.cpp
.The text was updated successfully, but these errors were encountered: