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
Exception in thread "main" java.lang.IllegalArgumentException: A symbol with name `x' already exists, with type: Int
at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_declare_function(Native Method)
at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5FormulaCreator.makeVariable(Mathsat5FormulaCreator.java:154)
at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5FormulaCreator.makeVariable(Mathsat5FormulaCreator.java:137)
at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5BooleanFormulaManager.makeVariableImpl(Mathsat5BooleanFormulaManager.java:37)
at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5BooleanFormulaManager.makeVariableImpl(Mathsat5BooleanFormulaManager.java:25)
at org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager.makeVariable(AbstractBooleanFormulaManager.java:63)
...
Whereas it works as expected for, e.g. Princess or Z3. I could imagine a solution where Mathsat5Formula is an intermediate representation of the formula that only gets "baked" into a MathSAT native formula when actually making a call to the prover, but that comes with some overhead, of course.
The text was updated successfully, but these errors were encountered:
So then the idea is that the JavaSMT user should either generate a new solver context for every SMT call, or otherwise implement some kind of unique renaming thing themselves?
MathSAT throws an exception if two variables with the same name and different sorts are ever declared. For example:
This snippet causes the exception:
Whereas it works as expected for, e.g. Princess or Z3. I could imagine a solution where
Mathsat5Formula
is an intermediate representation of the formula that only gets "baked" into a MathSAT native formula when actually making a call to the prover, but that comes with some overhead, of course.The text was updated successfully, but these errors were encountered: