merlin

And I can't reproduce the bug6 in the fse_repl. $ git log -1 commit da2f5cc Author: Nikolaj Bjorner [email protected] Date: Tue Jan 21 14:18:49 2020 -0600 remove spurious out NAME="Ubuntu"...

> Can you share the SMT file generated by storm when you run > `storm --reproduce=bug6 --seed=1595625837` Thanks for your reply. This is the SMT file generated by storm when...

> > bug6.zip > > When I click on this, I get "not found" I feel sorry to it. [bug6.zip](https://github.com/Practical-Formal-Methods/storm/files/6343970/bug6.zip)

> Yes you are right. Something seems wrong with bug6. > I can take a look at it on the weekend. Is this urgent ? Sincerely thanks! It's not urgent....

Maybe the same problem occurs in bug 18... [bug18.zip](https://github.com/Practical-Formal-Methods/storm/files/6349621/bug18.zip)

I'm sorry for that. But the combination of bv and arithmetic also seems to make yices error. I'm not sure if it is valuable. ``` $ cat case.smt2 (set-logic ALL)...

``` $ cat small.smt2 (declare-const x (Array Bool Int)) (declare-const x2 (Array Bool Int)) (declare-fun v () (Array Bool Int)) (assert (forall ((a Bool)) (or (distinct x x2 v) (>...

``` $ cat small.smt2 (set-option :tactic.default_tactic smt) (set-option :sat.euf true) (set-option :rewriter.arith_lhs true) (set-option :model_validate true) (declare-fun va () Real) (declare-fun r () Real) (declare-fun r2 () Real) (declare-fun a...

``` $ cat small.smt2 (declare-fun var2647 () Real) (declare-fun ar7 () Real) (assert (forall ((v Real)) (distinct (= v 0) (= 0 (+ var2647 ar7))))) (check-sat-using qsat) $ z3 tactic.default_tactic=smt...

``` $ cat delta.out.smt2 (declare-fun var1307 () (Array Bool Int)) (assert (forall ((var1306 (Array Bool Int)) (var107 Int)) (xor (= 0 (select (store var1306 (= var1306 var1307) 0) false)) (<...