We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent f8f7610 commit 0e5a54eCopy full SHA for 0e5a54e
src/solvers/refinement/string_refinement.cpp
@@ -612,6 +612,22 @@ decision_proceduret::resultt string_refinementt::dec_solve()
612
found_length.clear();
613
found_content.clear();
614
615
+ // Initial try without index set
616
+ decision_proceduret::resultt res=supert::dec_solve();
617
+ if(res==D_SATISFIABLE)
618
+ {
619
+ if(!check_axioms())
620
621
+ debug() << "check_SAT: got SAT but the model is not correct" << eom;
622
+ }
623
+ else
624
625
+ debug() << "check_SAT: the model is correct" << eom;
626
+ concretize_lengths();
627
+ return D_SATISFIABLE;
628
629
630
+
631
initial_index_set(universal_axioms);
632
update_index_set(cur);
633
cur.clear();
0 commit comments