I have tried to output my constraint formula into a smt2 file.
from pysmt.smtlib.script import *
s = smtlibscript_from_formula(f)
print(s) # or s.serialize(file_handle) to directly dump the smt2 code to file
s.to_file( "String_of_FileName" , daggify=True) # or s.serialize(file_handle) to directly dump the smt2 code to file
Then the warning message shows that:
"sys:1: UserWarning: The logic QF_BV is not reducible to any SMTLib2 standard logic. Proceeding with non-standard logic 'QF_BV'"
Will it matters anything, or it's Okey to ignore it?
P.S: the whole formula is constructed by Bit-Vector calculations.