Git Product home page Git Product logo

smtinterpol's Introduction

SMTInterpol

This is SMTInterpol, an interpolating SMT-solver developed at the university of Freiburg. You can find more information on the website

http://ultimate.informatik.uni-freiburg.de/smtinterpol/

Compilation

To compile SMTInterpol you need:

  • Java (at least version 1.6)
  • Apache ant

SMTInterpol comes with an ant build file that compiles the sources into a bin folder (will be created by the build), and creates a standalone jar. You can run it with

ant

Usage

To run SMTInterpol from command line you need the standalone jar. Run it as

java -jar smtinterpol.jar

and pass the necessary commands to the standard input of this process. Alternatively you can specify a SMTLIB 2 script file as argument to the process. In either case, SMTInterpol will parse and execute commands until it an exit command or the end of the input stream.

Integration into Eclipse

The source distribution of SMTInterpol is an Eclipse project. If you want to use this project, you can easily import it into Eclipse as "Existing Project into Workspace".

Reporting Bugs

You can report bugs using the bug-tracker at github. Please provide all needed information. This includes:

  • a description of the bug (e.g., crash, unsoundness, or feature-request),
  • a way to reproduce the bug (e.g., an interaction log with the solver via the LoggingScript provided with the sources).
(declare-fun in (using) SMTInterpol)

smtinterpol's People

Contributors

alexandernutz avatar cheshire avatar confectio avatar damien-zufferey-sonarsource avatar danieldietsch avatar heizmann avatar henkele avatar jhoenicke avatar kfriedberger avatar lcacace avatar mohr-m avatar rohlandm avatar schillic avatar tanjaschindler avatar

Stargazers

avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar

Watchers

avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar

Forkers

jhoenicke gartenzaun cheshire tanjaschindler joanna69 rprasathg alexandereric995 aehyvari kfriedberger vb6hobbyst7 serras stevefreecastler lf274 heeptilo itanisyza3255 lcacace damien-zufferey-sonarsource

smtinterpol's Issues

NullPointerException from getInterpolants

I'm getting the following trace SMTInterpol:

java.lang.NullPointerException
    at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.interpolate(Interpolator.java:457)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.getInterpolants(Interpolator.java:263)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.getInterpolants(SMTInterpol.java:1220)
    at de.uni_freiburg.informatik.ultimate.logic.NoopScript.getInterpolants(NoopScript.java:230)
    at de.uni_freiburg.informatik.ultimate.logic.LoggingScript.getInterpolants(LoggingScript.java:327)
    at jkind.engines.pdr.PdrSmt.getInterpolants(PdrSmt.java:317)
    at jkind.engines.pdr.PdrSmt.refine(PdrSmt.java:295)
    at jkind.engines.pdr.PdrSubengine.blockCube(PdrSubengine.java:104)
    at jkind.engines.pdr.PdrSubengine.run(PdrSubengine.java:71)

This doesn't happened when I run the smt2 file that is being logged. It only happens when I go through the API. I'm not sure how to go about getting an smt2 file that exhibits the same behavior.

NullPointerException in Interpolator.interpolate

With this file produced by CPAchecker, the following exception occurs with the latest SMTInterpol revision (OpenJDK 7):

java.lang.NullPointerException
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.interpolate(Interpolator.java:489)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.interpolate(Interpolator.java:478)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.interpolate(Interpolator.java:478)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.interpolate(Interpolator.java:478)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.interpolate(Interpolator.java:478)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.interpolate(Interpolator.java:462)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.interpolate(Interpolator.java:478)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.interpolate(Interpolator.java:478)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.getInterpolants(Interpolator.java:262)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.getInterpolants(SMTInterpol.java:1213)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:1998)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:853)
        at java_cup.runtime.LRParser.parse(Unknown Source)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:129)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:114)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:36)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.Main.main(Main.java:182)

NullPointerException for incremental LIA instance

Hi, for the following formula

(set-logic LIA) 
(declare-fun v0 () Bool)
(declare-fun v1 () Bool)
(assert (forall ((q0 Bool) (q1 Bool)) (not (xor q1 v1 v0 q0 q1 (> 100 13) v0 q1))))
(push 1)
(assert (=> v1 v1))
(pop 1)
(check-sat)

smtinterpol (commit 3f24148) throws a NullPointerException

Unexpected Exception: java.lang.NullPointerException
(error "java.lang.NullPointerException")

Another AssertionError with check-sat-assuming

The following snipped causes SMTInterpol (453d36e) to fail with an AssertionError:

SMTInterpol env = new SMTInterpol(new DefaultLogger(), () -> false);
env.setLogic(Logics.QF_AUFLIRA);
env.declareFun("A", new Sort[] {}, env.getTheory().getBooleanSort());
Term[] terms = new Term[] {env.term("A")};
env.checkSatAssuming(terms);
env.checkSat();
env.checkSatAssuming(terms);

Stacktrace:

Exception in thread "main" java.lang.AssertionError
at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.assume(DPLLEngine.java:1877)
at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.checkSatAssuming(SMTInterpol.java:492)

Strangely, the corresponding SMTlib-input does not trigger the problem:

(set-logic QF_AUFLIRA)
(declare-fun A () Bool)
(check-sat-assuming (A))
(check-sat)
(check-sat-assuming (A))

This issue might be related to #29.

ClassCastException from check-sat-assuming with annotated term.

The follwing snippet crashes SMTInterpol in revision fca3ef3:

(set-option :random-seed 42)
(set-option :produce-proofs true)
(set-logic QF_AUFLIRA)
(declare-fun A () Bool)
(declare-fun pred1 () Bool)
(assert (! (or A pred1) :named term_0))
(check-sat-assuming (pred1))

Output:

[...]
success
Unexpected Exception: java.lang.ClassCastException: de.uni_freiburg.informatik.ultimate.logic.AnnotatedTerm cannot be cast to de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm
(error "java.lang.ClassCastException: de.uni_freiburg.informatik.ultimate.logic.AnnotatedTerm cannot be cast to de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm")

IndexOutOfBoundsException for incremental LIA instance

Hi, for the following formula

(set-logic LIA) 
(declare-fun v4 () Bool)
(declare-fun v7 () Bool)
(declare-fun v10 () Bool)
(assert (not (exists ((q0 Bool) (q1 Int) (q2 Bool) (q3 Int)) (not (>= 6 q3)))))
(push 1)
(assert (xor v7 v10 (= v4 v7 ) v4 (not v10)))
(pop 1)
(check-sat)

smtinterpol (commit 3f24148) throws an IndexOutOfBoundsException

Unexpected Exception: java.lang.IndexOutOfBoundsException: Index: 0, Size: 0
(error "java.lang.IndexOutOfBoundsException: Index: 0, Size: 0")

Errors in ant build

The Javadoc construction during the ant build throws several errors:

  [javadoc] Constructing Javadoc information...
  [javadoc] Standard Doclet version 1.8.0_202
  [javadoc] Building tree for all the packages and classes...
  [javadoc] /storage/repos/smtinterpol/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/ApplicationTerm.java:33: error: reference not found
  [javadoc]  * {@link Script#term(String, java.math.BigInteger[], Sort, Term...)}.
  [javadoc]           ^
  [javadoc] /storage/repos/smtinterpol/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/ApplicationTerm.java:37: warning - Tag @link: can't find term(String, java.math.BigInteger[], Sort, Term...) in de.uni_freiburg.informatik.ultimate.logic.Script
  [javadoc] /storage/repos/smtinterpol/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Script.java:117: error: @param name not found
  [javadoc]      * @param constr The Name of the constructor.
  [javadoc]               ^
  [javadoc] /storage/repos/smtinterpol/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Script.java:120: warning: no @param for constructor
  [javadoc]     public FunctionSymbol getFunctionSymbol(String constructor);
  [javadoc]                           ^
  [javadoc] /storage/repos/smtinterpol/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Script.java:127: error: syntax error in reference
  [javadoc]      * @throws SMTLIBException.
  [javadoc]        ^
  [javadoc] /storage/repos/smtinterpol/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Script.java:133: error: @param name not found
  [javadoc]      * @param sort Sort of the datatypes.
  [javadoc]               ^
  [javadoc] /storage/repos/smtinterpol/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Script.java:136: error: syntax error in reference
  [javadoc]      * @throws SMTLIBException.
  [javadoc]        ^
  [javadoc] /storage/repos/smtinterpol/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Script.java:138: warning: no @param for numParams
  [javadoc]     public DataType datatype(String typename, int numParams)
  [javadoc]                     ^
  [javadoc] /storage/repos/smtinterpol/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Script.java:142: warning: no description for @param
  [javadoc]      * @param datatype
  [javadoc]        ^
  [javadoc] /storage/repos/smtinterpol/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Script.java:144: error: syntax error in reference
  [javadoc]      * @throws SMTLIBException.
  [javadoc]        ^
  [javadoc] /storage/repos/smtinterpol/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Script.java:150: warning: no description for @param
  [javadoc]      * @param datatypes
  [javadoc]        ^
  [javadoc] /storage/repos/smtinterpol/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Script.java:152: error: syntax error in reference
  [javadoc]      * @throws SMTLIBException.
  [javadoc]        ^
  [javadoc] /storage/repos/smtinterpol/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Script.java:154: warning: no @param for sortParams
  [javadoc]     public void declareDatatypes(DataType[] datatypes, DataType.Constructor[][] constrs, Sort[][] sortParams)
  [javadoc]                 ^
  [javadoc] /storage/repos/smtinterpol/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Script.java:450: warning: no description for @throws
  [javadoc]      * @throws SMTLIBException
  [javadoc]        ^
  [javadoc] /storage/repos/smtinterpol/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Script.java:452: warning: no @param for constructors
  [javadoc]     public Term match(final Term dataArg, final TermVariable[][] vars, final Term[] cases,
  [javadoc]                 ^
  [javadoc] Building index for all the packages and classes...
  [javadoc] Building index for all classes...
  [javadoc] Generating /storage/repos/smtinterpol/doc-smtinterpol/help-doc.html...
  [javadoc] 7 errors
  [javadoc] 8 warnings

NullPointerException for incremental NIA instance

Hi, for the following instance

(set-logic NIA)
(declare-fun v0 () Bool)
(declare-fun v1 () Bool)
(declare-fun v2 () Bool)
(declare-fun v5 () Bool)
(declare-fun v11 () Bool)
(declare-fun v12 () Bool)
(declare-fun v17 () Bool)
(declare-fun v18 () Bool)
(declare-fun i2 () Int)
(declare-fun i3 () Int)
(declare-fun i4 () Int)
(push 1)
(assert (exists ((q0 Int) (q1 Bool) (q2 Bool) (q3 Int)) (=> (or v17 q1 q2 q2 v0) (< q3 q0))))
(declare-fun v20 () Bool)
(assert (not (exists ((q4 Bool) (q5 Bool)) (= (< 35 i4) v0 v12))))
(assert (or (forall ((q4 Bool) (q5 Bool)) v18) (exists ((q4 Bool) (q5 Bool)) (not (or v5 q5 q5 q4 q5)))))
(declare-fun v21 () Bool)
(assert (forall ((q6 Bool)) (not (xor q6 v0 q6 v11 q6 q6 (or v21 (> i4 29) v21 v12) (< 35 i4) q6))))
(push 1)
(assert (not (exists ((q7 Int)) (> i4 29))))
(pop 1)
(check-sat)

smtinterpol (commit 3f24148) throws a NullPointerException

Unexpected Exception: java.lang.NullPointerException
(error "java.lang.NullPointerException")

Not sure if the root cause is the same with #50

Interface request: expose values contained in a model

Hi,

It is often convenient to be able to loop over a model, while SMTInterpol only provides an interface for evaluating terms over it.
Would it be possible to expose the interface to see which functions are defined in a model?
From what I see in the source code, it would be sufficient to simply expose (perhaps in an unmodifiable way) the mFuncVals value in the Model class.

AssertionError with check-sat-assuming

Using the following (already reduced) test file, SMTInterpol 2.1-335-g4c543a5 produces an AssertionError:

(set-logic QF_UFLIA)
(declare-fun g0 () Bool)
(declare-fun a (Int Int) Bool)
(define-fun b ((t Int)) Int (+ (+ 0 (ite (a 0 t) 1 0)) (ite (a 2 t) 1 0)))
(assert (let ((.cse0 (b 2))) (< .cse0 1)))
(check-sat-assuming (g0))

When executing java -ea -jar smtinterpol-2.1-335-g4c543a5.jar < test.smt2 the solver outputs the following lines:

success
success
success
success
INFO - Sharing term: 2
INFO - Sharing term: 0
success
Exception in thread "main" java.lang.AssertionError
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.getLevel0(DPLLEngine.java:1556)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.level0resolve(DPLLEngine.java:868)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.explainConflict(DPLLEngine.java:747)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.explain(DPLLEngine.java:858)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.solve(DPLLEngine.java:1215)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol$CheckType$1.check(SMTInterpol.java:115)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.checkSatAssuming(SMTInterpol.java:528)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2295)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:1146)
        at com.github.jhoenicke.javacup.runtime.LRParser.parse(Unknown Source)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:147)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:125)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:37)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.Main.main(Main.java:180)

As it seems to me, check-sat-assuming is the culprit here. Replacing (check-sat-assuming (g0)) with (assert g0) (check-sat) produces the correct result.

Consider Maven central release

Hi,

Would you consider releasing SMTInterpol to Maven Central? (http://search.maven.org/)
It's a most commonly used repository of Java projects, much like pypi for Python, or Debian repositories for Linux.
It doesn't require using Maven, and can be done from ANT.
Projects released to Maven central can be used in other Java projects by essentially adding one configuration line.
I can help with technical issues related to Maven Central release.

Regards,
George

Do not abort immediately for interpolation queries with theory of arrays

Commit 656452f (the merge of branch logger) has introduced three lines in SMTInterpol.java that let all interpolation queries fail immediately if the theory has arrays enabled. Previously SMTInterpol at least attempted to interpolate. It would be great if the previous behavior could be restored, because we simply always set the most general theory, and thus often have interpolation queries without any arrays, but the theory has arrays enabled.

:quotedLA leaks in some cases

Interpolants may contain terms annotated with :quotedLA although the user did not annotate it.

Example:
stmt-assume-2.bpl_AllErrorsAtOnce_Iteration2.smt2.txt

The interpolant we receive is:
((and (ite (<= (+ ULTIMATE.start_y_-1 (- 9)) 0) (<= 0 ULTIMATE.start_x_-1) (! (<= (+ ULTIMATE.start_y_-1 (- 10)) 0) :quotedLA)) (ite (not (<= ULTIMATE.start_x_-1 0)) (<= ULTIMATE.start_y_-1 10) (not (! (<= (+ ULTIMATE.start_x_-1 1) 0) :quotedLA)))) (and (let ((.cse0 (+ ULTIMATE.start_y_-1 (- 10)))) (ite (<= (+ ULTIMATE.start_y_-1 (- 9)) 0) (<= 0 .cse0) (! (<= .cse0 0) :quotedLA))) (let ((.cse1 (<= ULTIMATE.start_x_-1 0))) (ite (not .cse1) .cse1 (not (! (<= (+ ULTIMATE.start_x_-1 1) 0) :quotedLA))))) (and (let ((.cse0 (+ ULTIMATE.start_y_-1 (- 10)))) (ite (<= (+ ULTIMATE.start_y_-1 (- 9)) 0) (<= 0 .cse0) (! (<= .cse0 0) :quotedLA))) (let ((.cse1 (<= ULTIMATE.start_x_-1 0))) (ite (not .cse1) .cse1 (not (! (<= (+ ULTIMATE.start_x_-1 1) 0) :quotedLA))))))

The version is b24bab0

AssertionError: Not a unit clause

The queries with arrays in this gist produce stack traces like the following one:

java.lang.AssertionError: Not a unit clause: diva_dadapter_request::e@5 == diva_dadapter_request::e@4 in [!(*unsigned_char@8 == (store *unsigned_char@7 (+ |diva_dadapter_request::e@4| 1) 255)), !(*unsigned_char@7 == *unsigned_char@5), diva_dadapter_request::e@5 == diva_dadapter_request::e@4, !(*unsigned_char@8 == *unsigned_char@7), !(*unsigned_char@7 == (store *unsigned_char@6 (+ |diva_dadapter_request::e@5| 1) 255)), !(*unsigned_char@6 == (store *unsigned_char@5 (+ |diva_dadapter_request::e@4| 1) 7)), (select (store *unsigned_char@5 (+ |diva_dadapter_request::e@4| 1) 7) (+ |diva_dadapter_request::e@4| 1)) == (select (store *unsigned_char@5 (+ |diva_dadapter_request::e@4| 1) 255) (+ |diva_dadapter_request::e@4| 1))]
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.checkUnitClause(DPLLEngine.java:843)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.getExplanation(DPLLEngine.java:774)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.computeRedundancy(DPLLEngine.java:803)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.explainConflict(DPLLEngine.java:681)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.explain(DPLLEngine.java:749)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.solve(DPLLEngine.java:1079)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine$AllSatIterator.hasNext(DPLLEngine.java:1635)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.printResponse(ParseEnvironment.java:205)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2181)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:853)
        at java_cup.runtime.LRParser.parse(Unknown Source)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:129)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:114)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:40)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.Main.main(Main.java:182)

I have more examples for this problem, but this should hopefully be the two smallest ones.

NullPointerException for incremental UF instance

Hi, for the following formula

(set-logic UF)
(declare-fun v0 () Bool)
(declare-fun v3 () Bool)
(declare-fun v16 () Bool)
(assert (not (exists ((q4 Bool) (q5 Bool) (q6 Bool)) (not (xor q5 v16 q4 v0 (xor v16 v3) q5)))))
(push 1)
(check-sat)
(pop 1)
(check-sat)

smtinterpol (commit 3f24148) throws a NullPointerException

Unexpected Exception: java.lang.NullPointerException
(error "java.lang.NullPointerException")

ClassCastException for incremental UF and NRA instances

Hi, for the following formula

(set-logic UF)
(declare-fun v3 () Bool)
(declare-fun v4 () Bool)
(declare-fun v5 () Bool)
(declare-fun v14 () Bool)
(push 1)
(assert (xor v14 v4 v5 v3))
(declare-fun v21 () Bool)
(assert (or (forall ((q12 Bool) (q13 Bool) (q14 Bool) (q15 Bool)) (not (or q13 q12 q15 q15 q13 v21 q14 q13))) (exists ((q12 Bool) (q13 Bool) (q14 Bool) (q15 Bool)) (not (= v14 q15 (xor v14 v4 v5 v3) q13 q13)))))
(pop 1)
(assert (forall ((q54 Bool)) (not (= v14 q54 q54 v4 q54 (xor v3 v5) q54))))
(check-sat)

smtinterpol (commit 3f24148) throws a ClassCastException

Unexpected Exception: java.lang.ClassCastException: de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CCBaseTerm cannot be cast to de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CCAppTerm
(error "java.lang.ClassCastException: de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CCBaseTerm cannot be cast to de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CCAppTerm")

ProofTracker needs rewrite

There are several issues currently with the proof tracker.

Correctness Issues

The proof format using the full rewrite is

  • hard to verify (all rewrites have to be applied to the huge term dag)
  • wrong (some rewrite rules especially with SMTAffineTerm match at unintentioned
    sub terms)

This can be solved by a step-by-step rewrite system. I envision the following rewrite rules

(par (A) (@refl A Proof))
   ; returns for a term t a proof for (= t t)
(@trans Proof Proof Proof :left-assoc)
   ; returns for proofs (= a b) and (= b c) a proof (= a c)
(@cong Proof Proof Proof :left-assoc)  ; arguments are premises
   ; returns for proofs (= s (f t1 ... tn)) and (= t t')
   ; a proof for (= s (f t1' ... tn'))
   ; where ti' = t' if ti = t and ti'=ti otherwise.

Implementation Issues

Also the current performance of the proof tracker is bad. It repeatedly

  • cleans SMTAffineTerm (without caching, after hacking a cache
    into it, it runs much faster).
  • converts CCAppTerms to Terms when rewriting NamedAtoms
    (I added a cache in CCAppTerm, not the best place for this),
  • creates new @split terms.
    Currently, almost all the Clausifer.run() time is spent in ProofTracker.split, more precisely in creating @split terms (they make up less than 1% of the proof), and I have not yet found out why. Could be that most are not needed in the final proof, but my guess is that it creates the same @split term over and over again.

The code is also bad to analyse. The proof tracker uses only side-effects to create the proof, a functional interface would be better.

Minimum/maximum value that satisfies?

Hello.

Apologies if this isn't an appropriate place to ask, but I've not been able to find anywhere else to ask questions.

Is it possible to get the solver to optimize for a minimum and/or maximum value when trying to satisfy a problem?

Take the following trivial example:

(set-option :produce-assignments true)
(set-option :produce-proofs true)

(set-logic QF_LIA)

(declare-fun p () Int)

(assert (>= p 0))
(assert (<= p 23))

(check-sat)

(get-value (p))

If I run that locally here, the value of p is 0. That's obviously acceptable given the assertions I specified, but what if I want p to be the highest value it can be (23 in this case)?

I'm looking to use SMTInterpol to model version constraints in a software package system with statements like package p depends on package q version >= 1 <= 3 and would obviously prefer if the solver picked the largest values for all assignments that it could.

Simple solving with assumptions sends SMTInterpol into a loop

The bug is encountered on the following file (though, naturally, we go through the API)

(set-option :global-declarations true)
(set-option :random-seed 42)
(set-option :produce-interpolants true)
(set-option :produce-models true)
(set-option :produce-unsat-cores true)
(set-logic QF_AUFLIRA)
(get-option :random-seed)
(push 1)
(pop 1)
(pop 0)
(push 1)
(check-sat-assuming ())
(pop 1)
(pop 0)
(declare-fun v1 () Int)
(declare-fun v2 () Int)
(declare-fun suffix1 () Bool)
(declare-fun suffix2 () Bool)
(declare-fun suffix3 () Bool)
(get-option :random-seed)
(push 1)
(push 1)
(assert (! (or (and (= v1 1) (not (= v1 v2))) suffix1) :named term_0))
(push 1)
(assert (! (or (= v2 1) suffix2) :named term_1))
(push 1)
(assert (! (or (not (= v1 1)) suffix3) :named term_2))
(check-sat-assuming ((not suffix1) (not suffix2) suffix3))

Interpolator.colorLiterals is recursive

The method Interpolator.colorLiterals is recursive. AFAIK SMTInterpol prefers non-recursive algorithms to prevent stack overflows on large formulas, so you might want to change this method accordingly.

I have a single instance where this actually triggers a stack overflow for us in a few hundred seconds, so it is not very important, but I wanted to at least mention it.

C API

Not a bug, more of a feature request. Is there any plans of providing a C API to the solver? For integration into tools implemented in other languages C would be the cleanest way.

AssertionError at InstantiationManager.java:201

Hi, for the following formula
201.txt

smtinterpol (commit 686b165) throws an assertion error

success
Exception in thread "main" java.lang.AssertionError
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.quant.InstantiationManager.instantiateSomeNotSat(InstantiationManager.java:201)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.quant.QuantifierTheory.computeConflictClause(QuantifierTheory.java:242)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.checkConsistency(DPLLEngine.java:1018)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.solve(DPLLEngine.java:1165)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol$CheckType$1.check(SMTInterpol.java:113)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.checkSatAssuming(SMTInterpol.java:476)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.checkSat(SMTInterpol.java:429)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2896)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:1311)
        at com.github.jhoenicke.javacup.runtime.LRParser.parse(Unknown Source)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:154)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:133)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:37)

Unsoundness in LIA/tptp

Multiple benchmarks in LIA/tptp are unsound, e.g. LIA/tptp/ARI052=1.smt2. Should be in supported fragment.

AssertionError in ArrayTheory.merge()

We have found an AssertionError when solving some queries with arrays:

java.lang.AssertionError
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.ArrayTheory.merge(ArrayTheory.java:951)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.ArrayTheory.buildWeakEq(ArrayTheory.java:1099)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.ArrayTheory.checkpoint(ArrayTheory.java:578)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.propagateInternal(DPLLEngine.java:246)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.solve(DPLLEngine.java:1026)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine$AllSatIterator.hasNext(DPLLEngine.java:1635)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.printResponse(ParseEnvironment.java:205)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2181)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:853)
        at java_cup.runtime.LRParser.parse(Unknown Source)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:129)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:114)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:40)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.Main.main(Main.java:182)

This happens with the latest version 2.1-235-g3b87807. An input file for reproducing it is here: https://gist.github.com/PhilippWendler/7bfce5387a4c22b938f3 (it happens with a few different queries, but the stacktrace is always identical, thus I assume it is the same problem).

Endless loop due to branching on linear variables

Hi,

this is more of a "for your information" than a bug report, because the bug was already fixed.

With the following input, SMTInterpol does not terminate, but dies from an OutOfMemoryError (after a long time):

(set-logic QF_LIA)
(declare-fun var0 () Int)
(declare-fun var1 () Int)
(declare-fun var2 () Int)
(assert (and
   (> 0 (+ (* 2 var0) var2))
   (> 0 (+ var0 var2))
   (> 0 (+ (* (- 2) var0) (* (- 4) var1) (* (- 5) var2)))
   (> 0 (* (- 3) var1))
   (> 0 (+ (* (- 1) var0) (* (- 3) var1) (* (- 2) var2)))))
(check-sat)

I was using an older version (smtinterpol-2.1-149-g744cf8f) and noticed that the problem is already fixed in the latest version. A bisect tells me that db5d02a fixed this problem. I am only reporting this, because that commit talks about a negative effect on a benchmark while my issue is (in my opinion) a lot more severe than that. No idea if you want to use this as a unit test or something like that, but I just wanted to inform you that the commit fixed a more serious issue.

AssertionError in DPLLEngine.setLiteral

Attached script throws assertion error when assertions are enabled (java -ea -jar smtinterpol-2.5-638-g686b1653.jar).

Stack trace:

Exception in thread "main" java.lang.AssertionError
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.setLiteral(DPLLEngine.java:440)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.propagateTheories(DPLLEngine.java:290)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.propagateInternal(DPLLEngine.java:237)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.quickCheck(DPLLEngine.java:1691)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.assertTerm(SMTInterpol.java:656)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2881)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:1311)
        at com.github.jhoenicke.javacup.runtime.LRParser.parse(Unknown Source)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:154)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:133)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:37)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.Main.main(Main.java:180)

Script:
32_7_cilled_const_ok_linux-32_1-drivers--net--wireless--p54--p54usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i_AllErrorsAtOnce_Iteration6.smt2.txt

I can generate 11 more scripts from different files if necessary.

NullPointerException in MutableInfinitNumber.compareTo

I'm using version 2.1-217-g6d15196.

The following check-sat query causes a NullPointerException

(set-logic QF_UFLIRA)
(set-option :verbosity 2)
(declare-fun x () Real)
(assert (not (= (div (to_int x) 5) (to_int (/ x 5)))))
(check-sat)

java.lang.NullPointerException
    at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.linar.MutableInfinitNumber.compareTo(MutableInfinitNumber.java:147)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.linar.LinArSolve.choose(LinArSolve.java:2116)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.linar.LinArSolve.mutate(LinArSolve.java:1883)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.linar.LinArSolve.computeConflictClause(LinArSolve.java:609)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.checkConsistency(DPLLEngine.java:901)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.solve(DPLLEngine.java:1039)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol$CheckType$1.check(SMTInterpol.java:98)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.checkSat(SMTInterpol.java:759)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:1963)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:853)
    at java_cup.runtime.LRParser.parse(Unknown Source)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:129)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:114)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:40)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.Main.main(Main.java:182)

AssertionError in LinArSolve.mbtc(...)

SMTInterpol 2.5-40-g69ef504908 (build from 69ef504) crashes on the attached input script with a NullPointerException. When enabling assertions, the crash is an assertion error.

Stacktrace:

Exception in thread "main" java.lang.AssertionError
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.linar.LinArSolve.mbtc(LinArSolve.java:2061)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.linar.LinArSolve.computeConflictClause(LinArSolve.java:618)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.checkConsistency(DPLLEngine.java:1027)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.solve(DPLLEngine.java:1171)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol$CheckType$1.check(SMTInterpol.java:114)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.checkSatAssuming(SMTInterpol.java:502)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.checkSat(SMTInterpol.java:455)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2279)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:1146)
        at com.github.jhoenicke.javacup.runtime.LRParser.parse(Unknown Source)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:147)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:125)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:37)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.Main.main(Main.java:180)

ArrayIndexOutOfBounds in CutCreator

This file (217 MB!) produces ArrayIndexOutOfBounds in CutCreator. The fault seems to be in the incremental engine though. The tableaux is broken when the bug occurs. It contains a variable in the matrix that is no longer in the list of linear variables.

Strange model of unsat benchmark

Benchmark: UF/grasshopper/instantiated/copy_invariant_16_2.smt2

Script:

(set-option :print-success false)
(set-option :timeout 10000)
(set-option :verbosity 3)
(echo "instantiated/concat_check_heap_access_23_4.smt2")
(timed (include "instantiated/concat_check_heap_access_23_4.smt2"))
(reset)
(set-option :print-success false)
(set-option :timeout 10000)
(set-option :verbosity 7)
(echo "instantiated/copy_invariant_16_2.smt2")
(include "instantiated/copy_invariant_16_2.smt2")

Log:
UF_grasshopper_instantiated_copy_invariant_16_2.wrong_model.log

Escaping for reserved variable names

Hi All,

Creating a variable called select, or store, or true fails with SMTInterpol, with an error message "Function X already defined".
While it's true that this function is indeed already defined for arrays, I think the proper course of action is to apply an escaping mechanism with "|" symbols, which is already found in SMTInterpol.

All other solvers we have tested (Z3, Princess, Mathsat5) do apply such escaping themselves.

AssertionError in Clausifier.createLinVar

Attached script throws assertion error when assertions are enabled (java -ea -jar smtinterpol-2.5-638-g686b1653.jar).

Stack trace:

Exception in thread "main" java.lang.AssertionError
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.createLinVar(Clausifier.java:1114)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.EqualityProxy.createAtom(EqualityProxy.java:154)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.EqualityProxy.getLiteral(EqualityProxy.java:186)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.EqualityProxy.createCCEquality(EqualityProxy.java:109)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CCTerm.propagateSharedEquality(CCTerm.java:262)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CCTerm.share(CCTerm.java:238)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CClosure.addSharedTerm(CClosure.java:772)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.share(Clausifier.java:1003)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.shareLATerm(Clausifier.java:1011)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.createLinVar(Clausifier.java:1121)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.createMutableAffinTerm(Clausifier.java:1131)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.addTermAxioms(Clausifier.java:1076)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.EqualityProxy.createAtom(EqualityProxy.java:141)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.EqualityProxy.getLiteral(EqualityProxy.java:186)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier$CollectLiteral.perform(Clausifier.java:585)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.run(Clausifier.java:1879)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.addFormula(Clausifier.java:1946)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.assertTerm(SMTInterpol.java:650)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.InterpolantChecker.checkFinalInterpolants(InterpolantChecker.java:426)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.getInterpolants(Interpolator.java:221)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.getInterpolants(SMTInterpol.java:866)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2947)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:1311)
        at com.github.jhoenicke.javacup.runtime.LRParser.parse(Unknown Source)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:154)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:133)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:37)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.Main.main(Main.java:180)

Script:
list_search-2.i_AllErrorsAtOnce_Iteration12.smt2.txt

I can generate 2 more scripts if necessary.

NullPointerException on Interpolation

The following input causes SMTInterpol (version 2.5-7-g64ec65d and 2.5-43-gc407d0f) to fail with a NullPointerException:

(set-option :produce-interpolants true)
(set-logic QF_AUFLIRA)
(push 1)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(push 1)
(assert (! (= 1 a) :named term_0))
(assert (! (= a 0) :named term_1))
(assert (! (= b c) :named term_2))
(check-sat)
(get-interpolants term_2)

I know that the interpolation query is too short, but this could be checked by SMTInterpol before trying to compute an interpolant. For the given interpolation query I would expect an empty list as result (based on the scheme that N formulas return N-1 interpolants).

An additional question is:
What happens when only some of the asserted formulas are used in the interpolation query?
Is the rest considered as background theory and, e.g., automatically added to each single formula given in the interpolation query?
For example, can I find some documentation about the result of an intepolation query like (get-interpolants term_0 term_1) for the given example? Or is it undefined behaviour?

ClassCastException for incremental NRA instance

Hi, for the following formula

(set-logic NRA)
(declare-fun v0 () Bool)
(declare-fun v1 () Bool)
(declare-fun v2 () Bool)
(declare-fun v3 () Bool)
(declare-fun v4 () Bool)
(declare-fun v5 () Bool)
(declare-fun v6 () Bool)
(declare-fun v7 () Bool)
(declare-fun v8 () Bool)
(declare-fun v9 () Bool)
(declare-fun r0 () Real)
(declare-fun r7 () Real)
(declare-fun r10 () Real)
(push 1)
(declare-fun v10 () Bool)
(declare-fun r12 () Real)
(declare-fun v11 () Bool)
(assert (or (forall ((q3 Real)) (or v3 v7 v3)) (exists ((q3 Real)) v6)))
(assert (=> v4 v11))
(assert (exists ((q4 Real) (q5 Real) (q6 Bool) (q7 Bool)) (not (not v5))))
(assert (or (exists ((q4 Real) (q5 Real) (q6 Bool) (q7 Bool)) (>= 2530134.0 6913554.0)) (exists ((q4 Real) (q5 Real) (q6 Bool) (q7 Bool)) (not (distinct q4 q4)))))
(declare-fun r14 () Real)
(check-sat)
(pop 1)
(declare-fun v12 () Bool)
(assert (forall ((q8 Bool) (q9 Bool) (q10 Bool)) (not (and q9 v7 v3 q9 v4 v9 v8))))
(assert (or (forall ((q8 Bool) (q9 Bool) (q10 Bool)) (not (or v1 v3 q8 v5 v4 q10 q9 v4 v5))) (exists ((q8 Bool) (q9 Bool) (q10 Bool)) v12)))
(assert (and v12 v0 v12 v0 v4 v7 v1 v7 v12))
(push 1)
(assert (xor v2 v12 v12 v2 v2 v8 v0 (<= r0 r0 r10) v0 v9))
(check-sat)
(pop 1)
(declare-fun r15 () Real)
(assert (xor v12 v3 v7 v9 v12 v3 v2 v2 v2 v12))
(assert (or (forall ((q15 Real) (q16 Bool)) (=> (xor (not v12) q16 q16 q16 (= 7313772477.0 0.137156 r0) q16 v5 v0) (= r15 6599423.0 19974.0))) (exists ((q15 Real) (q16 Bool)) (=> (>= 15.0 q15 2530134.0) (and v8 q16 v9)))))
(push 1)
(check-sat)

smtinterpol (commit 3f24148) throws a ClassCastException

Unexpected Exception: java.lang.ClassCastException: de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CCBaseTerm cannot be cast to de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CCAppTerm
(error "java.lang.ClassCastException: de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CCBaseTerm cannot be cast to de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CCAppTerm")

AssertionError at theory.quant.QuantifierTheory.checkpoint(QuantifierTheory.java:191)

Hi, for the following formula

191.txt

smtinterpol (commit d768667) throws an assertion error

        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.quant.QuantifierTheory.checkpoint(QuantifierTheory.java:191)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.propagateInternal(DPLLEngine.java:257)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.solve(DPLLEngine.java:1154)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol$CheckType$1.check(SMTInterpol.java:113)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.checkSatAssuming(SMTInterpol.java:476)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.checkSat(SMTInterpol.java:429)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2896)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:1311)
        at com.github.jhoenicke.javacup.runtime.LRParser.parse(Unknown Source)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:154)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:133)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:37)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.Main.main(Main.java:180)

IndexOutOfBoundsException for incremental NIA instance

Hi, for the following formula

(set-logic NIA)
(declare-fun v0 () Bool)
(declare-fun v1 () Bool)
(declare-fun v2 () Bool)
(declare-fun v4 () Bool)
(declare-fun v5 () Bool)
(declare-fun v7 () Bool)
(declare-fun i0 () Int)
(declare-fun i1 () Int)
(declare-fun i5 () Int)
(declare-fun i7 () Int)
(assert v1)
(declare-fun v8 () Bool)
(assert (< 59 61))
(check-sat)
(declare-fun v10 () Bool)
(assert (=> v10 (< 52 i1)))
(assert (not (exists ((q0 Bool) (q1 Int) (q2 Int)) (not (>= 61 q2)))))
(push 1)
(push 1)
(assert (exists ((q7 Int)) (and v10 v4 v1 (xor (distinct i7 i5) v2 (=> v10 (< 52 i1)) v10 v4 v8 v7 v10 v0 v4 v5))))
(assert (forall ((q9 Bool) (q10 Int) (q11 Int)) (not (not q9))))
(pop 1)
(check-sat)
(push 1)
(check-sat)

smtinterpol (commit 3f24148) throws an IndexOutOfBoundsException

Unexpected Exception: java.lang.IndexOutOfBoundsException: Index: 1, Size: 1
(error "java.lang.IndexOutOfBoundsException: Index: 1, Size: 1")

NullPointerException for BV instance

Hi, for the following formula

(set-logic BV)
(declare-fun v2 () Bool)
(declare-fun v3 () Bool)
(declare-fun v10 () Bool)
(assert (not (exists ((q0 Bool) (q1 Bool) (q2 Bool) (q3 Bool)) (not (xor v3 q3 v10 v2 q3)))))
(check-sat)

smtinterpol (commit 3f24148) throws a NullPointerException

Unexpected Exception: java.lang.NullPointerException
(error "java.lang.NullPointerException")

Assertion on Interpolation in Branch `quantifiers`

The appended smt2-file causes an assertion when computing interpolants.

I used the latest version from the branch quantifiers and executed:

java -ea -jar dist/smtinterpol-2.5-532-g5379eb3.jar -q smtquery.000.txt

The result is an Assertion:

Exception in thread "main" java.lang.AssertionError
	at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator$MixedLAInterpolator.convert(Interpolator.java:923)
	at de.uni_freiburg.informatik.ultimate.logic.TermTransformer.cacheConvert(TermTransformer.java:131)
	at de.uni_freiburg.informatik.ultimate.logic.TermTransformer.access$000(TermTransformer.java:42)
	at de.uni_freiburg.informatik.ultimate.logic.TermTransformer$Convert.walk(TermTransformer.java:79)
	at de.uni_freiburg.informatik.ultimate.logic.NonRecursive.run(NonRecursive.java:115)
	at de.uni_freiburg.informatik.ultimate.logic.NonRecursive.run(NonRecursive.java:106)
	at de.uni_freiburg.informatik.ultimate.logic.TermTransformer.transform(TermTransformer.java:253)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.mixedPivotLA(Interpolator.java:1124)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.combine(Interpolator.java:371)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.access$200(Interpolator.java:60)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator$CombineInterpolants.walk(Interpolator.java:158)
	at de.uni_freiburg.informatik.ultimate.logic.NonRecursive.run(NonRecursive.java:115)
	at de.uni_freiburg.informatik.ultimate.logic.NonRecursive.run(NonRecursive.java:106)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.interpolate(Interpolator.java:238)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.getInterpolants(Interpolator.java:215)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.getInterpolants(SMTInterpol.java:863)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2330)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:1146)
	at com.github.jhoenicke.javacup.runtime.LRParser.parse(Unknown Source)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:155)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:133)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:37)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.Main.main(Main.java:180)

The branch is important for us, because the assertion also happens in the latest Maven-release, which was build from 2.5-515-g2765bdd2 that is part of the history of this branch.
We use that version from Maven in CPAchecker (see the corresponding issue).
Please either fix the assertion in the branch quantifiers or release a new Maven-build from the master-branch.

NullPointerException for several quantified instance( incremental mode)

Hi, for the following formula

(set-logic NRA)
(declare-fun v0 () Bool)
(declare-fun v1 () Bool)
(declare-fun v2 () Bool)
(declare-fun v3 () Bool)
(declare-fun v4 () Bool)
(declare-fun v5 () Bool)
(declare-fun v6 () Bool)
(declare-fun v7 () Bool)
(declare-fun r0 () Real)
(declare-fun r1 () Real)
(declare-fun r2 () Real)
(assert (not v3))
(check-sat)
(assert (or (>= r1 r2 r0) (>= r1 r2 r0) v5 v2 v2))
(declare-fun v10 () Bool)
(declare-fun v11 () Bool)
(assert (not (exists ((q3 Bool) (q4 Bool) (q5 Real) (q6 Bool)) (=> (>= q5 r1) (xor q4 q3 q3 v10 v11 q3 (or v4 (xor v7 v5 v7) v3 v5 v3 (not v3) v7 v4 v10))))))
(push 1)
(push 1)
(check-sat)
(pop 1)
(push 1)
(check-sat)

smtinterpol (commit 3f24148) throws a NullPointerException

Unexpected Exception: java.lang.NullPointerException
(error "java.lang.NullPointerException")

IndexOutOfBoundsException in ArrayValue.toSMTLIB

Input:

(set-option :print-success false)
(set-option :verbosity 3)
(get-info :version)
(set-logic QF_ALIA)
(declare-fun arr () (Array Int Int))
(define-fun m0 () Int (select arr 0))
(define-fun ba () Int (select arr 1))
(define-fun bb () Int (select arr 2))
(assert (>= (- m0 ba) 0))
(assert (< (- m0 bb) 0))
(check-sat)
(get-model)

Output:

(:version "2.1-149-g744cf8f")
sat
ERROR - Unexpected Exception
java.lang.IndexOutOfBoundsException
    at de.uni_freiburg.informatik.ultimate.smtinterpol.model.NumericSortInterpretation.get(NumericSortInterpretation.java:78)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.model.ArrayValue.toSMTLIB(ArrayValue.java:317)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.model.ArraySortInterpretation.get(ArraySortInterpretation.java:83)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.model.Model.toModelTerm(Model.java:270)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.model.ModelFormatter.appendFunctionValue(ModelFormatter.java:110)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.model.ModelFormatter.appendValue(ModelFormatter.java:90)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.model.Model.toString(Model.java:203)
    at java.lang.String.valueOf(String.java:2982)
    at java.io.PrintWriter.println(PrintWriter.java:754)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.printResponse(ParseEnvironment.java:211)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2043)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:853)
    at java_cup.runtime.LRParser.parse(Unknown Source)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:129)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:114)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:36)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.Main.main(Main.java:180)
(error "java.lang.IndexOutOfBoundsException")

AssertionError: passing these results is not yet implemented

The following example program throws the error mentioned in the title (using web interface). The problem seems to be the define of OLED_BUFSIZE as 128*64/8. When replacing it with 1024 the program goes through.

typedef unsigned char uint8_t;

#define OLED_WIDTH   128
#define OLED_HEIGHT  64
#define OLED_BUFSIZE (OLED_WIDTH * OLED_HEIGHT / 8)

static uint8_t _oledbuffer[OLED_BUFSIZE];


#define OLED_OFFSET(x, y) (OLED_BUFSIZE - 1 - (x) - ((y)/8)*OLED_WIDTH)
#define OLED_MASK(x, y) (1 << (7 - (y) % 8))

#define max(X,Y) ((X) > (Y) ? (X) : (Y))
#define min(X,Y) ((X) < (Y) ? (X) : (Y))

/*
 * Inverts pixel at x, y
 */
void oledInvertPixel(int x, int y)
{
        if ((x < 0) || (y < 0) || (x >= OLED_WIDTH) || (y >= OLED_HEIGHT)) {
                return;
        }
        _oledbuffer[OLED_OFFSET(x, y)] ^= OLED_MASK(x, y);
}
/*
 * Inverts box between (x1,y1) and (x2,y2) inclusive.
 */
void oledInvert(int x1, int y1, int x2, int y2)
{
        x1 = max(x1, 0);
        y1 = max(y1, 0);
        x2 = min(x2, OLED_WIDTH - 1);
        y2 = min(y2, OLED_HEIGHT - 1);
        for (int x = x1; x <= x2; x++) {
                for (int y = y1; y <= y2; y++) {
                        oledInvertPixel(x,y);
                }
        }
}

int getInt();

int main()
{
    oledInvert(getInt(), getInt(), getInt(), getInt());
}

Performance of FunctionSymbol.checkSort

In our application, we construct huge formulas where already the construction process takes thousands of seconds. The function FunctionSymbol.checkSort is a huge bottleneck in this case. Is the .toString() for comparing types really necessary? The formula consists of boolean variables only; why is it necessary to have the type check in this case?

Setting the log level of a DefaultLogger "does not really work"

Hi,

consider the following code:

DefaultLogger logger = new DefaultLogger(),
logger.setLoglevel(DefaultLogger.LOGLEVEL_OFF);
Script script = new SMTInterpol(logger);

What would be the expected result? No log messages.
What is the actual result? Log messages for level INFO and above.

It took me a moment to figure this out. The reason is that VerbosityOption's constructor activates the default log level. I suggest one of the following two patches to be applied (if you tell me which one you like, I can submit a pull request if you want me to):

Version 1: Just don't set the default log level. DefaultLogger already applies this in its constructor, so why set it again?

diff --git a/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/option/VerbosityOption.java b/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/option/VerbosityOption.java
index d4e43da..3bc4547 100644
--- a/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/option/VerbosityOption.java
+++ b/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/option/VerbosityOption.java
@@ -41,7 +41,7 @@ public class VerbosityOption extends Option {
        + "channel.  The bigger the number the more output will be produces.  0 "
                                + "turns off diagnostic output.");
                mLogger = logger;
-               mLogger.setLoglevel(mDefaultLvl = Config.DEFAULT_LOG_LEVEL);
+               mDefaultLvl = Config.DEFAULT_LOG_LEVEL;
        }
        @Override
        public Option copy() {

Version 2: Use whatever loglevel the logger has initially as the default level:

diff --git a/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/option/VerbosityOption.java b/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/option/VerbosityOption.java
index d4e43da..0df4e23 100644
--- a/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/option/VerbosityOption.java
+++ b/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/option/VerbosityOption.java
@@ -41,7 +41,7 @@ public class VerbosityOption extends Option {
        + "channel.  The bigger the number the more output will be produces.  0 "
                                + "turns off diagnostic output.");
                mLogger = logger;
-               mLogger.setLoglevel(mDefaultLvl = Config.DEFAULT_LOG_LEVEL);
+               mDefaultLvl = logger.getLoglevel();
        }
        @Override
        public Option copy() {

AssertionError at theory.linar.LinArSolve.choose(LinArSolve.java:1776)

Hi, for the following formula

smtinterpol (commit 686b165) throws an assertion error

eption in thread "main" java.lang.AssertionError
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.linar.LinArSolve.choose(LinArSolve.java:1776)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.linar.LinArSolve.mutate(LinArSolve.java:1673)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.linar.LinArSolve.computeConflictClause(LinArSolve.java:634)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.checkConsistency(DPLLEngine.java:1018)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.solve(DPLLEngine.java:1165)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol$CheckType$1.check(SMTInterpol.java:113)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.checkSatAssuming(SMTInterpol.java:476)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.checkSat(SMTInterpol.java:429)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2896)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:1311)
        at com.github.jhoenicke.javacup.runtime.LRParser.parse(Unknown Source)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:154)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:133)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:37)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.Main.main(Main.java:180)

NullPointerException in LAInterpolator.AnnotInfo.color

This file created by CPAchecker produces a NullPointerException with current SMTInterpol:

java.lang.NullPointerException
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.LAInterpolator$AnnotInfo.color(LAInterpolator.java:81)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.LAInterpolator$AnnotInfo.<init>(LAInterpolator.java:63)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.LAInterpolator.computeAuxAnnotations(LAInterpolator.java:163)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.LAInterpolator.computeAuxAnnotations(LAInterpolator.java:169)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.LAInterpolator.computeInterpolants(LAInterpolator.java:426)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.interpolate(Interpolator.java:568)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.interpolate(Interpolator.java:462)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.getInterpolants(Interpolator.java:262)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.getInterpolants(SMTInterpol.java:1211)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:1998)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:853)        at java_cup.runtime.LRParser.parse(Unknown Source)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:129)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:114)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:36)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.Main.main(Main.java:180)

AssertionError at theory.quant.QuantifierTheory.computeConflictClause(QuantifierTheory.java:235)

Hi, for the following formula
235.txt

smtinterpol (commit 686b165) throws an assertion error

Exception in thread "main" java.lang.AssertionError
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.quant.QuantifierTheory.computeConflictClause(QuantifierTheory.java:235)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.checkConsistency(DPLLEngine.java:1018)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.solve(DPLLEngine.java:1165)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol$CheckType$1.check(SMTInterpol.java:113)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.checkSatAssuming(SMTInterpol.java:476)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.checkSat(SMTInterpol.java:429)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2896)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:1311)
        at com.github.jhoenicke.javacup.runtime.LRParser.parse(Unknown Source)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:154)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:133)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:37)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.Main.main(Main.java:180)

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.